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 f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 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 f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )
thus ( X1,X2 are_separated implies ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) ) :: thesis: ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 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 f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) )
hence X1 misses X2 by TSEP_1:63; :: thesis: for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 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 f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y by A1, Th133, TSEP_1:63; :: thesis: verum

end;

thus ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 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 f1 being continuous Function of X1,Y ex f2 being continuous Function of X2,Y st f1 union f2 is not continuous Function of (X1 union X2),Y or X1,X2 are_separated )
assume A3: for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ; :: thesis: X1,X2 are_separated

now :: thesis: 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

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
reconsider f2 = g | X2 as continuous Function of X2,Y by A5;
reconsider f1 = g | X1 as continuous Function of X1,Y by A4;
g = f1 union f2 by Th126;
hence g is continuous Function of (X1 union X2),Y by A3; :: thesis: verum

end;

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

end;