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

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )

thus ( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) ) :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated ) :: thesis: verum

( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )

let X1, X2 be non empty SubSpace of X; :: thesis: ( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )

thus ( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) ) :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated )

proof

thus
( X1 misses X2 & ( for Y being non empty TopSpace
assume A1:
X1,X2 are_separated
; :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) )

hence X1 misses X2 by TSEP_1:63; :: thesis: for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y

X1,X2 are_weakly_separated by A1, TSEP_1:78;

hence for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y by Th117; :: thesis: verum

end;for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) )

hence X1 misses X2 by TSEP_1:63; :: thesis: for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y

X1,X2 are_weakly_separated by A1, TSEP_1:78;

hence for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y by Th117; :: thesis: verum

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ) implies X1,X2 are_separated ) :: thesis: verum

proof

assume A2:
X1 misses X2
; :: thesis: ( ex Y being non empty TopSpace ex f being Function of X,Y st

( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y & f | (X1 union X2) is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )

assume A3: for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ; :: thesis: X1,X2 are_separated

for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

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

end;( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y & f | (X1 union X2) is not continuous Function of (X1 union X2),Y ) or X1,X2 are_separated )

assume A3: for Y being non empty TopSpace

for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds

f | (X1 union X2) is continuous Function of (X1 union X2),Y ; :: thesis: X1,X2 are_separated

for Y being non empty TopSpace

for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

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

proof

hence
X1,X2 are_separated
by A2, Th123; :: thesis: verum
let Y be non empty TopSpace; :: thesis: for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds

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

let g be Function of (X1 union X2),Y; :: 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 )

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

consider h being Function of X,Y such that

A6: h | (X1 union X2) = g by Th57;

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

then A7: h | X2 is continuous Function of X2,Y by A5, A6, Th70;

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

then h | X1 is continuous Function of X1,Y by A4, A6, Th70;

hence g is continuous Function of (X1 union X2),Y by A3, A6, A7; :: thesis: verum

end;g is continuous Function of (X1 union X2),Y

let g be Function of (X1 union X2),Y; :: 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 )

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

consider h being Function of X,Y such that

A6: h | (X1 union X2) = g by Th57;

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

then A7: h | X2 is continuous Function of X2,Y by A5, A6, Th70;

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

then h | X1 is continuous Function of X1,Y by A4, A6, Th70;

hence g is continuous Function of (X1 union X2),Y by A3, A6, A7; :: thesis: verum