let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X = X1 union X2 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 is continuous Function of X,Y ) ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X = X1 union X2 implies ( 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 is continuous Function of X,Y ) ) ) )
assume A1: X = X1 union X2 ; :: 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 is continuous Function of X,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 is continuous Function of X,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 is continuous Function of X,Y ) implies X1,X2 are_separated )

proof

assume A2: 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 is continuous Function of X,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 is continuous Function of X,Y
X1,X2 are_weakly_separated by A2, 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 is continuous Function of X,Y by A1, Th120; :: 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 is continuous Function of X,Y ) implies X1,X2 are_separated ) :: thesis: verum

proof

assume A3: 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 is not continuous Function of X,Y ) or X1,X2 are_separated )
assume A4: 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 is continuous Function of X,Y ; :: thesis: X1,X2 are_separated
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

proof

let Y be non empty TopSpace; :: thesis: 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 f be Function of X,Y; :: thesis: ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y implies f | (X1 union X2) is continuous Function of (X1 union X2),Y )
assume ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ; :: thesis: f | (X1 union X2) is continuous Function of (X1 union X2),Y
then f is continuous Function of X,Y by A4;
hence f | (X1 union X2) is continuous Function of (X1 union X2),Y ; :: thesis: verum

end;

hence X1,X2 are_separated by A3, Th124; :: thesis: verum

end;