let X, Y be non empty TopSpace; 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; ( 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
; 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; ( 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; ( 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; verum