let X be TopSpace; :: thesis: for Y being non empty TopSpace
for A, B being closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y st f tolerates g holds
f +* g is continuous Function of (X | (A \/ B)),Y
let Y be non empty TopSpace; :: thesis: for A, B being closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y st f tolerates g holds
f +* g is continuous Function of (X | (A \/ B)),Y
let A, B be closed Subset of X; :: thesis: for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y st f tolerates g holds
f +* g is continuous Function of (X | (A \/ B)),Y
let f be continuous Function of (X | A),Y; :: thesis: for g being continuous Function of (X | B),Y st f tolerates g holds
f +* g is continuous Function of (X | (A \/ B)),Y
let g be continuous Function of (X | B),Y; :: thesis: ( f tolerates g implies f +* g is continuous Function of (X | (A \/ B)),Y )
assume A1: f tolerates g ; :: thesis: f +* g is continuous Function of (X | (A \/ B)),Y
A2: ( the carrier of (X | A) = A & the carrier of (X | B) = B & the carrier of (X | (A \/ B)) = A \/ B ) by PRE_TOPC:29;
then A3: ( dom (f +* g) = (dom f) \/ (dom g) & dom f = A & dom g = B ) by FUNCT_2:def 1, FUNCT_4:def 1;
( (rng f) \/ (rng g) c= the carrier of Y \/ the carrier of Y & rng (f +* g) c= (rng f) \/ (rng g) ) by FUNCT_4:18;
then reconsider h = f +* g as Function of (X | (A \/ B)),Y by A2, A3, FUNCT_2:4, XBOOLE_1:1;
h is continuous

proof

let C be Subset of Y; :: according to PRE_TOPC:def 12 :: thesis: ( not C is closed or h " C is closed )
assume C is closed ; :: thesis: h " C is closed
then A4: ( f " C is closed & g " C is closed ) by PRE_TOPC:def 12;
then consider C1 being Subset of X such that
A5: ( C1 is closed & C1 /\ ([#] (X | A)) = f " C ) by PRE_TOPC:43;
consider C2 being Subset of X such that
A6: ( C2 is closed & C2 /\ ([#] (X | B)) = g " C ) by A4, PRE_TOPC:43;
A7: ( [#] (X | (A \/ B)) = A \/ B & [#] (X | A) = A & [#] (X | B) = B ) by PRE_TOPC:29;
A8: h " C = (f " C) \/ (g " C) by A1, Th1
.= ((f " C) \/ (g " C)) /\ (A \/ B) by A7, XBOOLE_1:13, XBOOLE_1:28 ;
( C1 /\ A is closed & C2 /\ B is closed ) by A5, A6, TOPS_1:35;
then (C1 /\ A) \/ (C2 /\ B) is closed by TOPS_1:36;
hence h " C is closed by A5, A6, A7, A8, PRE_TOPC:43; :: thesis: verum

end;

hence f +* g is continuous Function of (X | (A \/ B)),Y ; :: thesis: verum