let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty open SubSpace of X st X1 misses X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
let X1, X2 be non empty open SubSpace of X; :: thesis: ( X1 misses X2 implies for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y )
assume A1: X1 misses X2 ; :: thesis: for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
let f1 be continuous Function of X1,Y; :: thesis: for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
let f2 be continuous Function of X2,Y; :: thesis: 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 Th116; :: thesis: verum