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 )

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

( 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

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 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;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

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

end;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

hence
X1,X2 are_separated
by A2, Th123; :: thesis: verumfor 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;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