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 )

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

( 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

thus
( X1 misses X2 & ( for Y being non empty TopSpace
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;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

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

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

hence
X1,X2 are_separated
by A3, Th124; :: thesis: verum
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;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