let X, Y be non empty TopSpace; for f being Function of X,Y
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated holds
( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
let f be Function of X,Y; for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated holds
( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
let X1, X2 be non empty SubSpace of X; ( X = X1 union X2 & X1,X2 are_weakly_separated implies ( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) )
assume that
A1:
X = X1 union X2
and
A2:
X1,X2 are_weakly_separated
; ( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
thus
( f is continuous Function of X,Y implies ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
; ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y implies f is continuous Function of X,Y )
assume
( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y )
; f is continuous Function of X,Y
then
f | (X1 union X2) is continuous Function of (X1 union X2),Y
by A2, Th117;
hence
f is continuous Function of X,Y
by A1, Th54; verum