let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty open SubSpace of X

for g being Function of (X1 union X2),Y holds

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

let X1, X2 be non empty open SubSpace of X; :: thesis: for g being Function of (X1 union X2),Y holds

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

let g be Function of (X1 union X2),Y; :: thesis: ( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

X1,X2 are_weakly_separated by TSEP_1:81;

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

for g being Function of (X1 union X2),Y holds

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

let X1, X2 be non empty open SubSpace of X; :: thesis: for g being Function of (X1 union X2),Y holds

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

let g be Function of (X1 union X2),Y; :: thesis: ( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )

X1,X2 are_weakly_separated by TSEP_1:81;

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