let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for X1, X2 being non empty open SubSpace of X st X = X1 union X2 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; :: thesis: for X1, X2 being non empty open SubSpace of X st X = X1 union X2 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 open SubSpace of X; :: thesis: ( X = X1 union X2 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 A1: X = X1 union X2 ; :: thesis: ( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
X1,X2 are_weakly_separated by TSEP_1:81;
hence ( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) by A1, Th120; :: thesis: verum