let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds

for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_weakly_separated implies for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ) )

assume A1: X1,X2 are_weakly_separated ; :: thesis: for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

let g be Function of (X1 union X2),Y; :: thesis: ( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;

A3: X1 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 A2, Th82; :: thesis: ( 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 )

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: verum

for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_weakly_separated implies for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) ) )

assume A1: X1,X2 are_weakly_separated ; :: thesis: for g being Function of (X1 union X2),Y holds

( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

let g be Function of (X1 union X2),Y; :: thesis: ( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;

A3: X1 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 A2, Th82; :: thesis: ( 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 )

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: verum

proof

assume that

A4: g | X1 is continuous Function of X1,Y and

A5: g | X2 is continuous Function of X2,Y ; :: thesis: g is continuous Function of (X1 union X2),Y

for x being Point of (X1 union X2) holds g is_continuous_at x

end;A4: g | X1 is continuous Function of X1,Y and

A5: g | X2 is continuous Function of X2,Y ; :: thesis: g is continuous Function of (X1 union X2),Y

for x being Point of (X1 union X2) holds g is_continuous_at x

proof

hence
g is continuous Function of (X1 union X2),Y
by Th44; :: thesis: verum
set X0 = X1 union X2;

let x be Point of (X1 union X2); :: thesis: g is_continuous_at x

A6: ( X1 meets X2 implies g is_continuous_at x )

end;let x be Point of (X1 union X2); :: thesis: g is_continuous_at x

A6: ( X1 meets X2 implies g is_continuous_at x )

proof

( X1 misses X2 implies g is_continuous_at x )
assume A7:
X1 meets X2
; :: thesis: g is_continuous_at x

end;A8: now :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies g is_continuous_at x )

assume A9:
( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 )
; :: thesis: g is_continuous_at x

then consider Y1, Y2 being non empty open SubSpace of X such that

A10: Y1 meet (X1 union X2) is SubSpace of X1 and

A11: Y2 meet (X1 union X2) is SubSpace of X2 and

A12: ( 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, A7, TSEP_1:89;

A13: ( Y2 meets X1 union X2 implies Y2 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;

A14: ( Y1 meets X1 union X2 implies Y1 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;

end;then consider Y1, Y2 being non empty open SubSpace of X such that

A10: Y1 meet (X1 union X2) is SubSpace of X1 and

A11: Y2 meet (X1 union X2) is SubSpace of X2 and

A12: ( 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, A7, TSEP_1:89;

A13: ( Y2 meets X1 union X2 implies Y2 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;

A14: ( Y1 meets X1 union X2 implies Y1 meet (X1 union X2) is open SubSpace of X1 union X2 ) by Th39;

A15: now :: thesis: ( X1 union X2 is not SubSpace of Y1 union Y2 implies g is_continuous_at x )

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 Th6;

assume A16: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: g is_continuous_at x

then consider Z being non empty closed SubSpace of X such that

A17: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Z and

A18: Z meet (X1 union X2) is SubSpace of X1 meet X2 by A12;

the carrier of (X1 union X2) c= the carrier of X12 by BORSUK_1:1;

then A19: X1 union X2 is SubSpace of X12 by TSEP_1:4;

then X12 meets X1 union X2 by Th17;

then A20: ((Y1 union Y2) union Z) meet (X1 union X2) = TopStruct(# the carrier of (X1 union X2), the topology of (X1 union X2) #) by A17, A19, TSEP_1:28;

A21: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) by A7, A9, A10, A11, A17, A18, Th32;

then ((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 A20, TSEP_1:32;

hence g is_continuous_at x by A22, A28, Th11; :: thesis: verum

end;then reconsider X12 = TopStruct(# the carrier of X, the topology of X #) as SubSpace of X by Th6;

assume A16: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: g is_continuous_at x

then consider Z being non empty closed SubSpace of X such that

A17: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Z and

A18: Z meet (X1 union X2) is SubSpace of X1 meet X2 by A12;

the carrier of (X1 union X2) c= the carrier of X12 by BORSUK_1:1;

then A19: X1 union X2 is SubSpace of X12 by TSEP_1:4;

then X12 meets X1 union X2 by Th17;

then A20: ((Y1 union Y2) union Z) meet (X1 union X2) = TopStruct(# the carrier of (X1 union X2), the topology of (X1 union X2) #) by A17, A19, TSEP_1:28;

A21: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) by A7, A9, A10, A11, A17, A18, Th32;

A22: now :: thesis: ( ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x implies g is_continuous_at x )

(Y1 union Y2) meet (X1 union X2) = (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) by A21, TSEP_1:32;

hence g is_continuous_at x by A27, A25, A23, Th11; :: thesis: verum

end;

A23: now :: thesis: ( ex x2 being Point of (Y2 meet (X1 union X2)) st x2 = x implies g is_continuous_at x )

given x2 being Point of (Y2 meet (X1 union X2)) such that A24:
x2 = x
; :: thesis: g is_continuous_at x

g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;

then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;

hence g is_continuous_at x by A7, A9, A10, A11, A13, A17, A18, A24, Th32, Th79; :: thesis: verum

end;g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;

then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;

hence g is_continuous_at x by A7, A9, A10, A11, A13, A17, A18, A24, Th32, Th79; :: thesis: verum

A25: now :: thesis: ( ex x1 being Point of (Y1 meet (X1 union X2)) st x1 = x implies g is_continuous_at x )

assume A27:
ex x12 being Point of ((Y1 union Y2) meet (X1 union X2)) st x12 = x
; :: thesis: g is_continuous_at xgiven x1 being Point of (Y1 meet (X1 union X2)) such that A26:
x1 = x
; :: thesis: g is_continuous_at x

g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;

then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;

hence g is_continuous_at x by A7, A9, A10, A11, A14, A17, A18, A26, Th32, Th79; :: thesis: verum

end;g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;

then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;

hence g is_continuous_at x by A7, A9, A10, A11, A14, A17, A18, A26, Th32, Th79; :: thesis: verum

(Y1 union Y2) meet (X1 union X2) = (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) by A21, TSEP_1:32;

hence g is_continuous_at x by A27, A25, A23, Th11; :: thesis: verum

A28: now :: thesis: ( ex x0 being Point of (Z meet (X1 union X2)) st x0 = x implies g is_continuous_at x )

( Y1 union Y2 meets X1 union X2 & Z meets X1 union X2 )
by A7, A9, A10, A11, A16, A17, A18, Th33;given x0 being Point of (Z meet (X1 union X2)) such that A29:
x0 = x
; :: thesis: g is_continuous_at x

consider x00 being Point of (X1 meet X2) such that

A30: x00 = x0 by A18, Th10;

consider x1 being Point of X1 such that

A31: x1 = x00 by A7, Th12;

consider x2 being Point of X2 such that

A32: x2 = x00 by A7, Th12;

( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) by A4, A5, Th44;

hence g is_continuous_at x by A29, A30, A31, A32, Th111; :: thesis: verum

end;consider x00 being Point of (X1 meet X2) such that

A30: x00 = x0 by A18, Th10;

consider x1 being Point of X1 such that

A31: x1 = x00 by A7, Th12;

consider x2 being Point of X2 such that

A32: x2 = x00 by A7, Th12;

( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) by A4, A5, Th44;

hence g is_continuous_at x by A29, A30, A31, A32, Th111; :: thesis: verum

then ((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 A20, TSEP_1:32;

hence g is_continuous_at x by A22, A28, Th11; :: thesis: verum

now :: thesis: ( X1 union X2 is SubSpace of Y1 union Y2 implies g is_continuous_at x )

hence
g is_continuous_at x
by A15; :: thesis: verumassume A33:
X1 union X2 is SubSpace of Y1 union Y2
; :: thesis: g is_continuous_at x

then A34: Y1 meets X1 union X2 by A9, A10, A11, Th31;

then Y1 union Y2 meets X1 union X2 by A34, Th18;

then A39: (Y1 union Y2) meet (X1 union X2) = X1 union X2 by A33, TSEP_1:28;

Y2 meets X1 union X2 by A9, A10, A11, A33, Th31;

then (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) = X1 union X2 by A34, A39, TSEP_1:32;

hence g is_continuous_at x by A37, A35, Th11; :: thesis: verum

end;then A34: Y1 meets X1 union X2 by A9, A10, A11, Th31;

A35: now :: thesis: ( ex x2 being Point of (Y2 meet (X1 union X2)) st x2 = x implies g is_continuous_at x )

given x2 being Point of (Y2 meet (X1 union X2)) such that A36:
x2 = x
; :: thesis: g is_continuous_at x

g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;

then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;

hence g is_continuous_at x by A9, A10, A11, A13, A33, A36, Th31, Th79; :: thesis: verum

end;g | (Y2 meet (X1 union X2)) is continuous by A2, A5, A11, Th83;

then g | (Y2 meet (X1 union X2)) is_continuous_at x2 ;

hence g is_continuous_at x by A9, A10, A11, A13, A33, A36, Th31, Th79; :: thesis: verum

A37: now :: thesis: ( ex x1 being Point of (Y1 meet (X1 union X2)) st x1 = x implies g is_continuous_at x )

Y1 is SubSpace of Y1 union Y2
by TSEP_1:22;given x1 being Point of (Y1 meet (X1 union X2)) such that A38:
x1 = x
; :: thesis: g is_continuous_at x

g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;

then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;

hence g is_continuous_at x by A9, A10, A11, A14, A33, A38, Th31, Th79; :: thesis: verum

end;g | (Y1 meet (X1 union X2)) is continuous by A3, A4, A10, Th83;

then g | (Y1 meet (X1 union X2)) is_continuous_at x1 ;

hence g is_continuous_at x by A9, A10, A11, A14, A33, A38, Th31, Th79; :: thesis: verum

then Y1 union Y2 meets X1 union X2 by A34, Th18;

then A39: (Y1 union Y2) meet (X1 union X2) = X1 union X2 by A33, TSEP_1:28;

Y2 meets X1 union X2 by A9, A10, A11, A33, Th31;

then (Y1 meet (X1 union X2)) union (Y2 meet (X1 union X2)) = X1 union X2 by A34, A39, TSEP_1:32;

hence g is_continuous_at x by A37, A35, Th11; :: thesis: verum

now :: thesis: ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 ) implies g is_continuous_at x )

hence g is_continuous_at x by A42, A40; :: thesis: verum

end;

hence
g is_continuous_at x
by A8; :: thesis: verumA40: now :: thesis: ( X2 is SubSpace of X1 implies g is_continuous_at x )

assume
X2 is SubSpace of X1
; :: thesis: g is_continuous_at x

then A41: 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 A4, Th44;

hence g is_continuous_at x by A41, Th81; :: thesis: verum

end;then A41: 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 A4, Th44;

hence g is_continuous_at x by A41, Th81; :: thesis: verum

A42: now :: thesis: ( X1 is SubSpace of X2 implies g is_continuous_at x )

assume
( X1 is SubSpace of X2 or X2 is SubSpace of X1 )
; :: thesis: g is_continuous_at xassume
X1 is SubSpace of X2
; :: thesis: g is_continuous_at x

then A43: 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 A5, Th44;

hence g is_continuous_at x by A43, Th81; :: thesis: verum

end;then A43: 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 A5, Th44;

hence g is_continuous_at x by A43, Th81; :: thesis: verum

hence g is_continuous_at x by A42, A40; :: thesis: verum

proof

hence
g is_continuous_at x
by A6; :: thesis: verum
assume
X1 misses X2
; :: thesis: g is_continuous_at x

then X1,X2 are_separated by A1, TSEP_1:78;

then consider Y1, Y2 being non empty open SubSpace of X such that

A44: X1 is SubSpace of Y1 and

A45: X2 is SubSpace of Y2 and

A46: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) by TSEP_1:77;

Y2 misses X1 by A44, A45, A46, Th30;

then A47: X2 is open SubSpace of X1 union X2 by A45, Th41;

then A50: X1 is open SubSpace of X1 union X2 by A44, Th41;

end;then X1,X2 are_separated by A1, TSEP_1:78;

then consider Y1, Y2 being non empty open SubSpace of X such that

A44: X1 is SubSpace of Y1 and

A45: X2 is SubSpace of Y2 and

A46: ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) by TSEP_1:77;

Y2 misses X1 by A44, A45, A46, Th30;

then A47: X2 is open SubSpace of X1 union X2 by A45, Th41;

A48: now :: thesis: ( ex x2 being Point of X2 st x2 = x implies g is_continuous_at x )

Y1 misses X2
by A44, A45, A46, Th30;given x2 being Point of X2 such that A49:
x2 = x
; :: thesis: g is_continuous_at x

g | X2 is_continuous_at x2 by A5, Th44;

hence g is_continuous_at x by A47, A49, Th79; :: thesis: verum

end;g | X2 is_continuous_at x2 by A5, Th44;

hence g is_continuous_at x by A47, A49, Th79; :: thesis: verum

then A50: X1 is open SubSpace of X1 union X2 by A44, Th41;

now :: thesis: ( ex x1 being Point of X1 st x1 = x implies g is_continuous_at x )

hence
g is_continuous_at x
by A48, Th11; :: thesis: verumgiven x1 being Point of X1 such that A51:
x1 = x
; :: thesis: g is_continuous_at x

g | X1 is_continuous_at x1 by A4, Th44;

hence g is_continuous_at x by A50, A51, Th79; :: thesis: verum

end;g | X1 is_continuous_at x1 by A4, Th44;

hence g is_continuous_at x by A50, A51, Th79; :: thesis: verum