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

for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated 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 SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated 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 SubSpace of X; :: thesis: ( X = X1 union X2 & X1,X2 are_weakly_separated 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 that

A1: X = X1 union X2 and

A2: X1,X2 are_weakly_separated ; :: 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 ) )

thus ( f is continuous Function of X,Y implies ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) ; :: thesis: ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y implies f is continuous Function of X,Y )

assume ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ; :: thesis: f is continuous Function of X,Y

then f | (X1 union X2) is continuous Function of (X1 union X2),Y by A2, Th117;

hence f is continuous Function of X,Y by A1, Th54; :: thesis: verum

for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated 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 SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated 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 SubSpace of X; :: thesis: ( X = X1 union X2 & X1,X2 are_weakly_separated 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 that

A1: X = X1 union X2 and

A2: X1,X2 are_weakly_separated ; :: 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 ) )

thus ( f is continuous Function of X,Y implies ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ) ; :: thesis: ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y implies f is continuous Function of X,Y )

assume ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) ; :: thesis: f is continuous Function of X,Y

then f | (X1 union X2) is continuous Function of (X1 union X2),Y by A2, Th117;

hence f is continuous Function of X,Y by A1, Th54; :: thesis: verum