let T, T1, T2, S be non empty TopSpace; :: thesis: for f being Function of T1,S
for g being Function of T2,S
for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object 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
for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object 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: for F1, F2 being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object 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 F1, F2 be Subset of T; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is continuous & g is continuous & ( for p being object 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: F1 = [#] T1 and
A4: F2 = [#] T2 and
A5: ([#] T1) \/ ([#] T2) = [#] T and
A6: F1 is closed and
A7: F2 is closed and
A8: f is continuous and
A9: g is continuous and
A10: for p being object 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;
A11: dom g = the carrier of T2 by FUNCT_2:def 1
.= [#] T2 ;
A12: dom f = the carrier of T1 by FUNCT_2:def 1
.= [#] T1 ;
then A13: dom (f +* g) = [#] T by A5, A11, FUNCT_4:def 1
.= the carrier of T ;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then reconsider h = f +* g as Function of T,S by A13, FUNCT_2:2, XBOOLE_1:1;
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 )
set P3 = f " P;
set P4 = g " P;
[#] T1 c= [#] T by A5, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A5, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A14: dom h = (dom f) \/ (dom g) by FUNCT_4:def 1;

A15: 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 A16: x in (h " P) /\ ([#] T2) ; :: thesis: x in g " P
then x in h " P by XBOOLE_0:def 4;
then A17: h . x in P by FUNCT_1:def 7;
g . x = h . x by A11, A16, FUNCT_4:13;
hence x in g " P by A11, A16, A17, FUNCT_1:def 7; :: thesis: verum

end;

assume A18: x in g " P ; :: thesis: x in (h " P) /\ ([#] T2)
then A19: x in dom g by FUNCT_1:def 7;
g . x in P by A18, FUNCT_1:def 7;
then A20: h . x in P by A19, FUNCT_4:13;
x in dom h by A14, A19, XBOOLE_0:def 3;
then x in h " P by A20, FUNCT_1:def 7;
hence x in (h " P) /\ ([#] T2) by A18, XBOOLE_0:def 4; :: thesis: verum

end;

A21: 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 A22: 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 A23: x in [#] T2 ; :: thesis: h . x = f . x

then x in ([#] T1) /\ ([#] T2) by A22, XBOOLE_0:def 4;
then f . x = g . x by A10;
hence h . x = f . x by A11, A23, FUNCT_4:13; :: thesis: verum

end;

suppose not x in [#] T2 ; :: thesis: h . x = f . x

hence h . x = f . x by A11, FUNCT_4:11; :: 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 A24: x in (h " P) /\ ([#] T1) ; :: thesis: x in f " P
then x in h " P by XBOOLE_0:def 4;
then A25: h . x in P by FUNCT_1:def 7;
f . x = h . x by A21, A24;
hence x in f " P by A12, A24, A25, FUNCT_1:def 7; :: thesis: verum

end;

assume A26: x in f " P ; :: thesis: x in (h " P) /\ ([#] T1)
then x in dom f by FUNCT_1:def 7;
then A27: x in dom h by A14, XBOOLE_0:def 3;
f . x in P by A26, FUNCT_1:def 7;
then h . x in P by A21, A26;
then x in h " P by A27, FUNCT_1:def 7;
hence x in (h " P) /\ ([#] T1) by A26, XBOOLE_0:def 4; :: thesis: verum

end;

then A28: (h " P) /\ ([#] T1) = f " P by TARSKI:2;
assume A29: P is closed ; :: thesis: h " P is closed
then f " P is closed by A8, PRE_TOPC:def 6;
then ex F01 being Subset of T st
( F01 is closed & f " P = F01 /\ ([#] T1) ) by A1, PRE_TOPC:13;
then A30: P1 is closed by A3, A6;
g " P is closed by A9, A29, PRE_TOPC:def 6;
then ex F02 being Subset of T st
( F02 is closed & g " P = F02 /\ ([#] T2) ) by A2, PRE_TOPC:13;
then A31: P2 is closed by A4, A7;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A12, A11, A14, RELAT_1:132, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then h " P = (f " P) \/ (g " P) by A28, A15, TARSKI:2;
hence h " P is closed by A30, A31; :: thesis: verum

end;

hence h is continuous by PRE_TOPC:def 6; :: thesis: verum