let S, T, T1, T2, Y be non empty TopSpace; :: thesis: for f being Function of [:Y,T1:],S
for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let f be Function of [:Y,T1:],S; :: thesis: for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let g be Function of [:Y,T2:],S; :: thesis: for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let F1, F2 be closed Subset of T; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) implies ex h being Function of [:Y,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: f is continuous and
A7: g is continuous and
A8: for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ; :: thesis: ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
A9: dom f = the carrier of [:Y,T1:] by FUNCT_2:def 1;
set h = f +* g;
A10: the carrier of [:Y,T2:] = [: the carrier of Y, the carrier of T2:] by BORSUK_1:def 2;
A11: [:Y,T2:] is SubSpace of [:Y,T:] by A2, BORSUK_3:15;
A12: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
A13: dom g = the carrier of [:Y,T2:] by FUNCT_2:def 1;
A14: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
A15: the carrier of [:Y,T1:] = [: the carrier of Y, the carrier of T1:] by BORSUK_1:def 2;
then A16: dom (f +* g) = [: the carrier of Y, the carrier of T:] by A5, A10, A9, A13, A14, ZFMISC_1:97;
A17: the carrier of [:Y,T:] = [: the carrier of Y, the carrier of T:] by BORSUK_1:def 2;
then reconsider h = f +* g as Function of [:Y,T:],S by A16, A12, FUNCT_2:2, XBOOLE_1:1;
take h ; :: thesis: ( h = f +* g & h is continuous )
thus h = f +* g ; :: thesis: h is continuous
A18: [:Y,T1:] is SubSpace of [:Y,T:] by A1, BORSUK_3:15;
for P being Subset of S st P is closed holds
h " P is closed

proof

reconsider M = [:([#] Y),F1:] as Subset of [:Y,T:] ;
let P be Subset of S; :: thesis: ( P is closed implies h " P is closed )

A19: now :: thesis: for x being object holds
( ( x in (h " P) /\ ([#] [:Y,T2:]) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] [:Y,T2:]) ) )

let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] [:Y,T2:]) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] [:Y,T2:]) ) )
thus ( x in (h " P) /\ ([#] [:Y,T2:]) implies x in g " P ) :: thesis: ( x in g " P implies x in (h " P) /\ ([#] [:Y,T2:]) )

proof

assume A20: x in (h " P) /\ ([#] [:Y,T2:]) ; :: thesis: x in g " P
then x in h " P by XBOOLE_0:def 4;
then A21: h . x in P by FUNCT_1:def 7;
g . x = h . x by A13, A20, FUNCT_4:13;
hence x in g " P by A13, A20, A21, FUNCT_1:def 7; :: thesis: verum

end;

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

end;

A25: for x being set st x in [#] [:Y,T1:] holds
h . x = f . x

proof

let x be set ; :: thesis: ( x in [#] [:Y,T1:] implies h . x = f . x )
assume A26: x in [#] [:Y,T1:] ; :: thesis: h . x = f . x

now :: thesis: h . x = f . x

per cases ( x in [#] [:Y,T2:] or not x in [#] [:Y,T2:] ) ;

suppose A27: x in [#] [:Y,T2:] ; :: thesis: h . x = f . x

then x in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) by A26, XBOOLE_0:def 4;
then f . x = g . x by A8;
hence h . x = f . x by A13, A27, FUNCT_4:13; :: thesis: verum

end;

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

hence h . x = f . x by A13, 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) /\ ([#] [:Y,T1:]) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] [:Y,T1:]) ) )

let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] [:Y,T1:]) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] [:Y,T1:]) ) )
thus ( x in (h " P) /\ ([#] [:Y,T1:]) implies x in f " P ) :: thesis: ( x in f " P implies x in (h " P) /\ ([#] [:Y,T1:]) )

proof

assume A28: x in (h " P) /\ ([#] [:Y,T1:]) ; :: thesis: x in f " P
then x in h " P by XBOOLE_0:def 4;
then A29: h . x in P by FUNCT_1:def 7;
x in [#] [:Y,T1:] by A28;
then A30: x in dom f by FUNCT_2:def 1;
f . x = h . x by A25, A28;
hence x in f " P by A29, A30, FUNCT_1:def 7; :: thesis: verum

end;

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

end;

then A33: (h " P) /\ ([#] [:Y,T1:]) = f " P by TARSKI:2;
the carrier of T2 is Subset of T by A2, TSEP_1:1;
then [#] [:Y,T2:] c= [#] [:Y,T:] by A17, A10, ZFMISC_1:95;
then reconsider P2 = g " P as Subset of [:Y,T:] by XBOOLE_1:1;
the carrier of T1 is Subset of T by A1, TSEP_1:1;
then [#] [:Y,T1:] c= [#] [:Y,T:] by A17, A15, ZFMISC_1:95;
then reconsider P1 = f " P as Subset of [:Y,T:] by XBOOLE_1:1;
assume A34: P is closed ; :: thesis: h " P is closed
then f " P is closed by A6, PRE_TOPC:def 6;
then A35: ex F01 being Subset of [:Y,T:] st
( F01 is closed & f " P = F01 /\ ([#] [:Y,T1:]) ) by A18, PRE_TOPC:13;
h " P = (h " P) /\ (([#] [:Y,T1:]) \/ ([#] [:Y,T2:])) by A17, A9, A13, A14, A16, XBOOLE_1:28
.= ((h " P) /\ ([#] [:Y,T1:])) \/ ((h " P) /\ ([#] [:Y,T2:])) by XBOOLE_1:23 ;
then A36: h " P = (f " P) \/ (g " P) by A33, A19, TARSKI:2;
( M is closed & [#] [:Y,T1:] = [:([#] Y),F1:] ) by A3, Th15, BORSUK_3:1;
then A37: P1 is closed by A35;
g " P is closed by A7, A34, PRE_TOPC:def 6;
then A38: ex F02 being Subset of [:Y,T:] st
( F02 is closed & g " P = F02 /\ ([#] [:Y,T2:]) ) by A11, PRE_TOPC:13;
reconsider M = [:([#] Y),F2:] as Subset of [:Y,T:] ;
( M is closed & [#] [:Y,T2:] = [:([#] Y),F2:] ) by A4, Th15, BORSUK_3:1;
then P2 is closed by A38;
hence h " P is closed by A36, A37; :: thesis: verum

end;

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