let S, T be non empty TopSpace; :: thesis:
let T1, T2 be SubSpace of T; :: thesis:
let p1, p2 be Point of T; :: thesis:
let f be Function of T1,S; :: thesis:
let g be Function of T2,S; :: thesis:
assume that
A1: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} ) and
A2: T1 is compact and
A3: T2 is compact and
A4: T is Hausdorff and
A5: f is continuous and
A6: g is continuous and
A7: ( f . p1 = g . p1 & f . p2 = g . p2 ) ; :: thesis:
set h = f +* g;
A8: dom f = [#] T1 by FUNCT_2:def 1;
A9: dom g = [#] T2 by FUNCT_2:def 1;
then A10: dom (f +* g) = the carrier of T by A1, A8, FUNCT_4:def 1;
( (rng f) \/ (rng g) c= the carrier of S & rng (f +* g) c= (rng f) \/ (rng g) ) by FUNCT_4:18;
then rng (f +* g) c= the carrier of S by XBOOLE_1:1;
then reconsider h = f +* g as Function of T,S by A10, FUNCT_2:def 1, RELSET_1:11;
for P being Subset of S st P is closed holds
h " P is closed

let P be Subset of S; :: thesis:
assume A11: P is closed ; :: thesis:
A12: ( h " P c= dom h & dom h = (dom f) \/ (dom g) ) by FUNCT_4:def 1, RELAT_1:167;
then A13: h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A8, A9, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
A14: for x being set st x in [#] T1 holds
h . x = f . x

let x be set ; :: thesis:
assume A15: x in [#] T1 ; :: thesis:

per cases ;

suppose A16: x in [#] T2 ; :: thesis:

then A17: x in ([#] T1) /\ ([#] T2) by A15, XBOOLE_0:def 4;

per cases by A1, A17, TARSKI:def 2;

suppose x = p1 ; :: thesis:

hence h . x = f . x by A7, A9, A16, FUNCT_4:14; :: thesis:

end;

suppose x = p2 ; :: thesis:

hence h . x = f . x by A7, A9, A16, FUNCT_4:14; :: thesis:

end;

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

end;

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

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

end;

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

end;

now

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

assume x in (h " P) /\ ([#] T1) ; :: thesis:
then ( x in h " P & x in dom f & x in [#] T1 ) by A8, XBOOLE_0:def 4;
then ( h . x in P & x in dom f & f . x = h . x ) by A14, FUNCT_1:def 13;
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 & h . x in P ) by A12, A14, XBOOLE_0:def 3;
then ( x in h " P & x in [#] T1 ) by FUNCT_1:def 13;
hence x in (h " P) /\ ([#] T1) by XBOOLE_0:def 4; :: thesis:

end;

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

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

assume x in (h " P) /\ ([#] T2) ; :: thesis:
then ( x in h " P & x in dom g & x in [#] T2 ) by A9, XBOOLE_0:def 4;
then ( h . x in P & x in dom g & g . x = h . x ) by 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 & h . x in P ) by A12, FUNCT_4:14, XBOOLE_0:def 3;
then ( x in h " P & x in [#] T2 ) by FUNCT_1:def 13;
hence x in (h " P) /\ ([#] T2) by XBOOLE_0:def 4; :: thesis:

end;

then A19: h " P = (f " P) \/ (g " P) by A13, A18, TARSKI:2;
( f " P c= [#] T1 & [#] T1 c= [#] T ) by A1, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
( g " P c= [#] T2 & [#] T2 c= [#] T ) by A1, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
( f " P is closed & g " P is closed ) by A5, A6, A11, PRE_TOPC:def 12;
then ( f " P is compact & g " P is compact ) by A2, A3, Th17;
then ( P1 is compact & P2 is compact ) by Th42;
hence h " P is closed by A4, A19, Th16, Th19; :: thesis:

end;

hence f +* g is continuous Function of T,S by PRE_TOPC:def 12; :: thesis: