let X, Y be non empty TopSpace; :: thesis:
let X1, X2 be non empty SubSpace of X; :: thesis:
assume A1: X1,X2 are_weakly_separated ; :: thesis:
let g be Function of (X1 union X2),Y; :: thesis:
A2: ( X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 ) by TSEP_1:22;
hence ( g is continuous Function of (X1 union X2),Y implies ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ) by Th89; :: thesis:
thus ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y implies g is continuous Function of (X1 union X2),Y ) :: thesis:

proof

assume A3: ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ; :: thesis:
for x being Point of (X1 union X2) holds g is_continuous_at x

proof

let x be Point of (X1 union X2); :: thesis:
set X0 = X1 union X2;
A4: ( X1 misses X2 implies g is_continuous_at x )

proof

assume X1 misses X2 ; :: thesis:
then X1,X2 are_separated by A1, TSEP_1:85;
then consider Y1, Y2 being non empty open SubSpace of X such that
A5: ( X1 is SubSpace of Y1 & X2 is SubSpace of Y2 ) and
A6: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) by TSEP_1:83;
( Y1 misses X2 & Y2 misses X1 ) by A5, A6, Th35;
then A7: ( X1 is open SubSpace of X1 union X2 & X2 is open SubSpace of X1 union X2 ) by A5, Th46;

A8: now

given x1 being Point of X1 such that A9: x1 = x ; :: thesis:
g | X1 is_continuous_at x1 by A3, Th49;
hence g is_continuous_at x by A7, A9, Th86; :: thesis:

end;

now

given x2 being Point of X2 such that A10: x2 = x ; :: thesis:
g | X2 is_continuous_at x2 by A3, Th49;
hence g is_continuous_at x by A7, A10, Th86; :: thesis:

end;

hence g is_continuous_at x by A8, Th16; :: thesis:

end;

( X1 meets X2 implies g is_continuous_at x )

proof

assume A11: X1 meets X2 ; :: thesis:

A12: now

assume A13: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 ) ; :: thesis:

A14: now

assume X1 is SubSpace of X2 ; :: thesis:
then A15: TopStruct(# the carrier of X2,the topology of X2 #) = X1 union X2 by TSEP_1:23;
then reconsider x2 = x as Point of X2 ;
g | X2 is_continuous_at x2 by A3, Th49;
hence g is_continuous_at x by A15, Th88; :: thesis:

end;

now

assume X2 is SubSpace of X1 ; :: thesis:
then A16: TopStruct(# the carrier of X1,the topology of X1 #) = X1 union X2 by TSEP_1:23;
then reconsider x1 = x as Point of X1 ;
g | X1 is_continuous_at x1 by A3, Th49;
hence g is_continuous_at x by A16, Th88; :: thesis:

end;

hence g is_continuous_at x by A13, A14; :: thesis:

end;

now

assume A17: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis:
then consider Y1, Y2 being non empty open SubSpace of X such that
A18: Y1 meet (X1 union X2) is SubSpace of X1 and
A19: Y2 meet (X1 union X2) is SubSpace of X2 and
A20: ( X1 union X2 is SubSpace of Y1 union Y2 or ex Z being non empty closed SubSpace of X st
( TopStruct(# the carrier of X,the topology of X #) = (Y1 union Y2) union Z & Z meet (X1 union X2) is SubSpace of X1 meet X2 ) ) by A1, A11, TSEP_1:96;
A21: ( Y1 meets X1 union X2 implies Y1 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th44;
A22: ( Y2 meets X1 union X2 implies Y2 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th44;

A23: now

assume A24: X1 union X2 is SubSpace of Y1 union Y2 ; :: thesis:
then A25: Y1 meets X1 union X2 by A17, A18, A19, Th36;
A26: Y2 meets X1 union X2 by A17, A18, A19, A24, Th36;
Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
then Y1 union Y2 meets X1 union X2 by A25, Th23;
then (Y1 union Y2) meet (X1 union X2) = X1 union X2 by A24, TSEP_1:31;
then A27: (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) = X1 union X2 by A25, A26, TSEP_1:35;

A28: now

given x1 being Point of (Y1 meet (X1 union X2)) such that A29: x1 = x ; :: thesis:
g | (Y1 meet (X1 union X2)) is continuous by A2, A3, A18, Th90;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 by Th49;
hence g is_continuous_at x by A17, A18, A19, A21, A24, A29, Th36, Th86; :: thesis:

end;

now

given x2 being Point of (Y2 meet (X1 union X2)) such that A30: x2 = x ; :: thesis:
g | (Y2 meet (X1 union X2)) is continuous by A2, A3, A19, Th90;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 by Th49;
hence g is_continuous_at x by A17, A18, A19, A22, A24, A30, Th36, Th86; :: thesis:

end;

hence g is_continuous_at x by A27, A28, Th16; :: thesis:

end;

now

assume A31: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis:
then consider Z being non empty closed SubSpace of X such that
A32: TopStruct(# the carrier of X,the topology of X #) = (Y1 union Y2) union Z and
A33: Z meet (X1 union X2) is SubSpace of X1 meet X2 by A20;
A34: Y1 union Y2 meets X1 union X2 by A11, A17, A18, A19, A31, A32, A33, Th38;
A35: Z meets X1 union X2 by A11, A17, A18, A19, A31, A32, A33, Th38;
A36: Y1 meets X1 union X2 by A11, A17, A18, A19, A32, A33, Th37;
A37: Y2 meets X1 union X2 by A11, A17, A18, A19, A32, A33, Th37;
X is SubSpace of X by TSEP_1:2;
then reconsider X12 = TopStruct(# the carrier of X,the topology of X #) as SubSpace of X by Th11;
the carrier of (X1 union X2) c= the carrier of X12 by BORSUK_1:35;
then A38: X1 union X2 is SubSpace of X12 by TSEP_1:4;
then X12 meets X1 union X2 by Th22;
then ((Y1 union Y2) union Z) meet (X1 union X2) = TopStruct(# the carrier of (X1 union X2),the topology of (X1 union X2) #) by A32, A38, TSEP_1:31;
then A39: ((Y1 union Y2) meet (X1 union X2)) union (Z meet (X1 union X2)) = TopStruct(# the carrier of (X1 union X2),the topology of (X1 union X2) #) by A34, A35, TSEP_1:35;

A40: now

assume A41: ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x ; :: thesis:
A42: (Y1 union Y2) meet (X1 union X2) = (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) by A36, A37, TSEP_1:35;

A43: now

given x1 being Point of (Y1 meet (X1 union X2)) such that A44: x1 = x ; :: thesis:
g | (Y1 meet (X1 union X2)) is continuous by A2, A3, A18, Th90;
then g | (Y1 meet (X1 union X2)) is_continuous_at x1 by Th49;
hence g is_continuous_at x by A11, A17, A18, A19, A21, A32, A33, A44, Th37, Th86; :: thesis:

end;

now

given x2 being Point of (Y2 meet (X1 union X2)) such that A45: x2 = x ; :: thesis:
g | (Y2 meet (X1 union X2)) is continuous by A2, A3, A19, Th90;
then g | (Y2 meet (X1 union X2)) is_continuous_at x2 by Th49;
hence g is_continuous_at x by A11, A17, A18, A19, A22, A32, A33, A45, Th37, Th86; :: thesis:

end;

hence g is_continuous_at x by A41, A42, A43, Th16; :: thesis:

end;

now

given x0 being Point of (Z meet (X1 union X2)) such that A46: x0 = x ; :: thesis:
consider x00 being Point of (X1 meet X2) such that
A47: x00 = x0 by A33, Th15;
consider x1 being Point of X1 such that
A48: x1 = x00 by A11, Th17;
consider x2 being Point of X2 such that
A49: x2 = x00 by A11, Th17;
( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) by A3, Th49;
hence g is_continuous_at x by A46, A47, A48, A49, Th123; :: thesis:

end;

hence g is_continuous_at x by A39, A40, Th16; :: thesis:

end;

hence g is_continuous_at x by A23; :: thesis:

end;

hence g is_continuous_at x by A12; :: thesis:

end;

hence g is_continuous_at x by A4; :: thesis:

end;

hence g is continuous Function of (X1 union X2),Y by Th49; :: thesis:

end;