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

proof

let P be Subset of S; :: thesis:
assume A17: P is closed ; :: thesis:
A18: h " P = (h " P) /\ (([#] [:T1,Y:]) \/ ([#] [:T2,Y:])) by A10, A13, A14, A15, A16, XBOOLE_1:28
.= ((h " P) /\ ([#] [:T1,Y:])) \/ ((h " P) /\ ([#] [:T2,Y:])) by XBOOLE_1:23 ;
A19: for x being set st x in [#] [:T1,Y:] holds
h . x = f . x

proof

let x be set ; :: thesis:
assume A20: x in [#] [:T1,Y:] ; :: thesis:

now

per cases ;

suppose A21: x in [#] [:T2,Y:] ; :: thesis:

then x in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) by A20, XBOOLE_0:def 4;
then f . x = g . x by A8;
hence h . x = f . x by A14, A21, FUNCT_4:14; :: thesis:

end;

suppose not x in [#] [:T2,Y:] ; :: thesis:

hence h . x = f . x by A14, FUNCT_4:12; :: thesis:

end;

hence h . x = f . x ; :: thesis:

end;

now

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

proof

assume x in (h " P) /\ ([#] [:T1,Y:]) ; :: thesis:
then ( x in h " P & x in [#] [:T1,Y:] ) by XBOOLE_0:def 4;
then ( h . x in P & x in dom f & f . x = h . x ) by A19, FUNCT_1:def 13, FUNCT_2:def 1;
hence x in f " P by FUNCT_1:def 13; :: thesis:

end;

assume x in f " P ; :: thesis:
then ( x in dom f & f . x in P ) by FUNCT_1:def 13;
then ( x in dom h & x in [#] [:T1,Y:] & h . x in P ) by A15, A19, XBOOLE_0:def 3;
then ( x in h " P & x in [#] [:T1,Y:] ) by FUNCT_1:def 13;
hence x in (h " P) /\ ([#] [:T1,Y:]) by XBOOLE_0:def 4; :: thesis:

end;

then A22: (h " P) /\ ([#] [:T1,Y:]) = f " P by TARSKI:2;

now

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

proof

assume x in (h " P) /\ ([#] [:T2,Y:]) ; :: thesis:
then ( x in h " P & x in [#] [:T2,Y:] ) by XBOOLE_0:def 4;
then ( h . x in P & x in dom g & g . x = h . x ) by A14, FUNCT_1:def 13, FUNCT_4:14;
hence x in g " P by FUNCT_1:def 13; :: thesis:

end;

assume x in g " P ; :: thesis:
then ( x in dom g & g . x in P ) by FUNCT_1:def 13;
then ( x in dom h & x in [#] [:T2,Y:] & h . x in P ) by A15, FUNCT_4:14, XBOOLE_0:def 3;
then ( x in h " P & x in [#] [:T2,Y:] ) by FUNCT_1:def 13;
hence x in (h " P) /\ ([#] [:T2,Y:]) by XBOOLE_0:def 4; :: thesis:

end;

then A23: h " P = (f " P) \/ (g " P) by A18, A22, TARSKI:2;
the carrier of T1 is Subset of T by A1, TSEP_1:1;
then ( f " P c= [#] [:T1,Y:] & [#] [:T1,Y:] c= [#] [:T,Y:] ) by A10, A11, ZFMISC_1:118;
then reconsider P1 = f " P as Subset of [:T,Y:] by XBOOLE_1:1;
the carrier of T2 is Subset of T by A2, TSEP_1:1;
then ( g " P c= [#] [:T2,Y:] & [#] [:T2,Y:] c= [#] [:T,Y:] ) by A10, A12, ZFMISC_1:118;
then reconsider P2 = g " P as Subset of [:T,Y:] by XBOOLE_1:1;
f " P is closed by A6, A17, PRE_TOPC:def 12;
then consider F01 being Subset of [:T,Y:] such that
A24: ( F01 is closed & f " P = F01 /\ ([#] [:T1,Y:]) ) by A9, PRE_TOPC:43;
reconsider M = [:F1,([#] Y):] as Subset of [:T,Y:] ;
A25: M is closed by Th16;
[#] [:T1,Y:] = [:F1,([#] Y):] by A3, BORSUK_3:1;
then A26: P1 is closed by A24, A25, TOPS_1:35;
g " P is closed by A7, A17, PRE_TOPC:def 12;
then consider F02 being Subset of [:T,Y:] such that
A27: ( F02 is closed & g " P = F02 /\ ([#] [:T2,Y:]) ) by A9, PRE_TOPC:43;
reconsider M = [:F2,([#] Y):] as Subset of [:T,Y:] ;
A28: M is closed by Th16;
[#] [:T2,Y:] = [:F2,([#] Y):] by A4, BORSUK_3:1;
then P2 is closed by A27, A28, TOPS_1:35;
hence h " P is closed by A23, A26, TOPS_1:36; :: thesis:

end;

hence h is continuous by PRE_TOPC:def 12; :: thesis: