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

for f1 being continuous Function of X1,Y

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

f1 union f2 is continuous Function of (X1 union X2),Y

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

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

f1 union f2 is continuous Function of (X1 union X2),Y )

assume A1: X1 meets X2 ; :: thesis: for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) 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 st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds

f1 union f2 is continuous Function of (X1 union X2),Y

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

assume f1 | (X1 meet X2) = f2 | (X1 meet X2) ; :: thesis: f1 union f2 is continuous Function of (X1 union X2),Y

then ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) by A1, Th128;

hence f1 union f2 is continuous Function of (X1 union X2),Y by Th115; :: thesis: verum

for f1 being continuous Function of X1,Y

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

f1 union f2 is continuous Function of (X1 union X2),Y

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

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

f1 union f2 is continuous Function of (X1 union X2),Y )

assume A1: X1 meets X2 ; :: thesis: for f1 being continuous Function of X1,Y

for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) 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 st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds

f1 union f2 is continuous Function of (X1 union X2),Y

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

assume f1 | (X1 meet X2) = f2 | (X1 meet X2) ; :: thesis: f1 union f2 is continuous Function of (X1 union X2),Y

then ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) by A1, Th128;

hence f1 union f2 is continuous Function of (X1 union X2),Y by Th115; :: thesis: verum