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

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let X1, X2 be non empty SubSpace of X; :: thesis: ( X = X1 union X2 implies for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y )

assume A1: X = X1 union X2 ; :: thesis: for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let f1 be continuous Function of X1,Y; :: thesis: for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let f2 be continuous Function of X2,Y; :: thesis: ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X,Y )

assume A2: ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) ; :: thesis: ( not X1,X2 are_weakly_separated or f1 union f2 is continuous Function of X,Y )

reconsider g = f1 union f2 as Function of X,Y by A1;

assume A3: X1,X2 are_weakly_separated ; :: thesis: f1 union f2 is continuous Function of X,Y

( g | X1 = f1 & g | X2 = f2 ) by A1, A2, Def5;

hence f1 union f2 is continuous Function of X,Y by A1, A3, Th120; :: thesis: verum

for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let X1, X2 be non empty SubSpace of X; :: thesis: ( X = X1 union X2 implies for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y )

assume A1: X = X1 union X2 ; :: thesis: for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let f1 be continuous Function of X1,Y; :: thesis: for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds

f1 union f2 is continuous Function of X,Y

let f2 be continuous Function of X2,Y; :: thesis: ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of X,Y )

assume A2: ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) ; :: thesis: ( not X1,X2 are_weakly_separated or f1 union f2 is continuous Function of X,Y )

reconsider g = f1 union f2 as Function of X,Y by A1;

assume A3: X1,X2 are_weakly_separated ; :: thesis: f1 union f2 is continuous Function of X,Y

( g | X1 = f1 & g | X2 = f2 ) by A1, A2, Def5;

hence f1 union f2 is continuous Function of X,Y by A1, A3, Th120; :: thesis: verum