let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y

for X1, X2 being non empty closed SubSpace of X holds

( f | (X1 union X2) is continuous Function of (X1 union X2),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 closed SubSpace of X holds

( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )

let X1, X2 be non empty closed SubSpace of X; :: thesis: ( f | (X1 union X2) is continuous Function of (X1 union X2),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:80;

hence ( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) by Th117; :: thesis: verum

for X1, X2 being non empty closed SubSpace of X holds

( f | (X1 union X2) is continuous Function of (X1 union X2),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 closed SubSpace of X holds

( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )

let X1, X2 be non empty closed SubSpace of X; :: thesis: ( f | (X1 union X2) is continuous Function of (X1 union X2),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:80;

hence ( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) by Th117; :: thesis: verum