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

for f being Function of X,Y 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 SubSpace of X; :: thesis: ( X1,X2 are_weakly_separated implies for f being Function of X,Y 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 ) ) )

assume A1: X1,X2 are_weakly_separated ; :: thesis: for f being Function of X,Y 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: ( 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 ) )

A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;

then A3: (f | (X1 union X2)) | X2 = f | X2 by Th71;

A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;

then A5: (f | (X1 union X2)) | X1 = f | X1 by Th71;

hence ( f | (X1 union X2) is continuous Function of (X1 union X2),Y implies ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) by A4, A2, A3, Th82; :: 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 )

thus ( 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 ) by A1, A5, A3, Th114; :: thesis: verum

for f being Function of X,Y 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 SubSpace of X; :: thesis: ( X1,X2 are_weakly_separated implies for f being Function of X,Y 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 ) ) )

assume A1: X1,X2 are_weakly_separated ; :: thesis: for f being Function of X,Y 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: ( 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 ) )

A2: X2 is SubSpace of X1 union X2 by TSEP_1:22;

then A3: (f | (X1 union X2)) | X2 = f | X2 by Th71;

A4: X1 is SubSpace of X1 union X2 by TSEP_1:22;

then A5: (f | (X1 union X2)) | X1 = f | X1 by Th71;

hence ( f | (X1 union X2) is continuous Function of (X1 union X2),Y implies ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) by A4, A2, A3, Th82; :: 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 )

thus ( 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 ) by A1, A5, A3, Th114; :: thesis: verum