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 )

proof

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;

thus ( 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 ) :: 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

proof

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;

hence X1,X2 are_separated by A2, Th123; :: thesis: verum

end;