let X, Y be non empty TopSpace; for X1, X2 being non empty SubSpace of X st X1 misses X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y
let X1, X2 be non empty SubSpace of X; ( X1 misses X2 implies for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y )
assume A1:
X1 misses X2
; for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y
let f1 be continuous Function of X1,Y; for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y
let f2 be continuous Function of X2,Y; ( X1,X2 are_weakly_separated implies f1 union f2 is continuous Function of (X1 union X2),Y )
assume A2:
X1,X2 are_weakly_separated
; f1 union f2 is continuous Function of (X1 union X2),Y
( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 )
by A1, Def12;
hence
f1 union f2 is continuous Function of (X1 union X2),Y
by A2, Th114; verum