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 ;
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 ; :: 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 ; :: thesis: verum
end;