let T, T1, T2, S be non empty TopSpace; :: thesis: for f being Function of T1,S
for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) holds
ex h being Function of T,S st
( h = f +* g & h is continuous )

let f be Function of T1,S; :: thesis: for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) holds
ex h being Function of T,S st
( h = f +* g & h is continuous )

let g be Function of T2,S; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) implies ex h being Function of T,S st
( h = f +* g & h is continuous ) )

assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: ([#] T1) \/ ([#] T2) = [#] T and
A4: T1 is compact and
A5: T2 is compact and
A6: T is T_2 and
A7: f is continuous and
A8: g is continuous and
A9: for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ; :: thesis: ex h being Function of T,S st
( h = f +* g & h is continuous )

set h = f +* g;
A10: dom g = [#] T2 by FUNCT_2:def 1;
A11: dom f = [#] T1 by FUNCT_2:def 1;
then A12: dom (f +* g) = the carrier of T by ;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then reconsider h = f +* g as Function of T,S by ;
take h ; :: thesis: ( h = f +* g & h is continuous )
thus h = f +* g ; :: thesis: h is continuous
for P being Subset of S st P is closed holds
h " P is closed
proof
let P be Subset of S; :: thesis: ( P is closed implies h " P is closed )
reconsider P3 = f " P as Subset of T1 ;
reconsider P4 = g " P as Subset of T2 ;
[#] T1 c= [#] T by ;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by ;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def 1;
A14: now :: thesis: for x being object holds
( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )
let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )
thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) :: thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )
proof
assume A15: x in (h " P) /\ ([#] T2) ; :: thesis: x in g " P
then x in h " P by XBOOLE_0:def 4;
then A16: h . x in P by FUNCT_1:def 7;
g . x = h . x by ;
hence x in g " P by ; :: thesis: verum
end;
assume A17: x in g " P ; :: thesis: x in (h " P) /\ ([#] T2)
then A18: x in dom g by FUNCT_1:def 7;
g . x in P by ;
then A19: h . x in P by ;
x in dom h by ;
then x in h " P by ;
hence x in (h " P) /\ ([#] T2) by ; :: thesis: verum
end;
A20: for x being set st x in [#] T1 holds
h . x = f . x
proof
let x be set ; :: thesis: ( x in [#] T1 implies h . x = f . x )
assume A21: x in [#] T1 ; :: thesis: h . x = f . x
now :: thesis: h . x = f . x
per cases ( x in [#] T2 or not x in [#] T2 ) ;
suppose A22: x in [#] T2 ; :: thesis: h . x = f . x
then x in ([#] T1) /\ ([#] T2) by ;
then f . x = g . x by A9;
hence h . x = f . x by ; :: thesis: verum
end;
suppose not x in [#] T2 ; :: thesis: h . x = f . x
hence h . x = f . x by ; :: thesis: verum
end;
end;
end;
hence h . x = f . x ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )
let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )
thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) :: thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )
proof
assume A23: x in (h " P) /\ ([#] T1) ; :: thesis: x in f " P
then x in h " P by XBOOLE_0:def 4;
then A24: h . x in P by FUNCT_1:def 7;
f . x = h . x by ;
hence x in f " P by ; :: thesis: verum
end;
assume A25: x in f " P ; :: thesis: x in (h " P) /\ ([#] T1)
then x in dom f by FUNCT_1:def 7;
then A26: x in dom h by ;
f . x in P by ;
then h . x in P by ;
then x in h " P by ;
hence x in (h " P) /\ ([#] T1) by ; :: thesis: verum
end;
then A27: (h " P) /\ ([#] T1) = f " P by TARSKI:2;
assume A28: P is closed ; :: thesis: h " P is closed
then P3 is closed by A7;
then P3 is compact by ;
then A29: P1 is compact by ;
P4 is closed by ;
then P4 is compact by ;
then A30: P2 is compact by ;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then h " P = (f " P) \/ (g " P) by ;
hence h " P is closed by A6, A29, A30; :: thesis: verum
end;
hence h is continuous ; :: thesis: verum