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 and
A2: ([#] T1) /\ ([#] T2) = {p1,p2} and
A3: T1 is compact and
A4: T2 is compact and
A5: T is Hausdorff and
A6: f is continuous and
A7: g is continuous and
A8: f . p1 = g . p1 and
A9: f . p2 = g . p2 ; :: thesis:
set h = f +* g;
A10: dom g = [#] T2 by FUNCT_2:def 1;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then A11: rng (f +* g) c= the carrier of S by XBOOLE_1:1;
A12: dom f = [#] T1 by FUNCT_2:def 1;
then dom (f +* g) = the carrier of T by A1, A10, FUNCT_4:def 1;
then reconsider h = f +* g as Function of T,S by A11, FUNCT_2:def 1, RELSET_1:4;
for P being Subset of S st P is closed holds
h " P is closed

let P be Subset of S; :: thesis:
[#] T1 c= [#] T by A1, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A1, XBOOLE_1:7;
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

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

assume A15: x in (h " P) /\ ([#] T2) ; :: thesis:
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 A10, A15, FUNCT_4:13;
hence x in g " P by A10, A15, A16, FUNCT_1:def 7; :: thesis:

end;

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

end;

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

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

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

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

per cases by A2, A23, TARSKI:def 2;

suppose x = p1 ; :: thesis:

hence h . x = f . x by A8, A10, A22, FUNCT_4:13; :: thesis:

end;

suppose x = p2 ; :: thesis:

hence h . x = f . x by A9, A10, A22, FUNCT_4:13; :: thesis:

end;

end;

end;

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

end;

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

hence h . x = f . x by A10, FUNCT_4:11; :: thesis:

end;

end;

end;

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

end;

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

assume A24: x in (h " P) /\ ([#] T1) ; :: thesis:
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 A20, A24;
hence x in f " P by A12, A24, A25, FUNCT_1:def 7; :: thesis:

end;

assume A26: x in f " P ; :: thesis:
then x in dom f by FUNCT_1:def 7;
then A27: x in dom h by A13, XBOOLE_0:def 3;
f . x in P by A26, FUNCT_1:def 7;
then h . x in P by A20, 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:

end;

then A28: (h " P) /\ ([#] T1) = f " P by TARSKI:1;
assume A29: P is closed ; :: thesis:
then f " P is closed by A6, PRE_TOPC:def 6;
then f " P is compact by A3, Th17;
then A30: P1 is compact by Th28;
g " P is closed by A7, A29, PRE_TOPC:def 6;
then g " P is compact by A4, Th17;
then A31: P2 is compact by Th28;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A12, A10, A13, 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, A14, TARSKI:1;
hence h " P is closed by A5, A30, A31; :: thesis:

end;

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