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 \/ B)) = A \/ B by PRE_TOPC:8;
the carrier of (X | B) = B by PRE_TOPC:8;
then A3: dom g = B by FUNCT_2:def 1;
the carrier of (X | A) = A by PRE_TOPC:8;
then A4: dom f = A by FUNCT_2:def 1;
A5: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def 1;
then reconsider h = f +* g as Function of (X | (A \/ B)),Y by A5, A2, A4, A3, FUNCT_2:2, XBOOLE_1:1;
h is continuous

proof

let C be Subset of Y; :: according to PRE_TOPC:def 6 :: thesis: ( not C is closed or h " C is closed )
A6: [#] (X | (A \/ B)) = A \/ B by PRE_TOPC:8;
assume A7: C is closed ; :: thesis: h " C is closed
then f " C is closed by PRE_TOPC:def 6;
then consider C1 being Subset of X such that
A8: C1 is closed and
A9: C1 /\ ([#] (X | A)) = f " C by PRE_TOPC:13;
g " C is closed by A7, PRE_TOPC:def 6;
then consider C2 being Subset of X such that
A10: C2 is closed and
A11: C2 /\ ([#] (X | B)) = g " C by PRE_TOPC:13;
A12: (C1 /\ A) \/ (C2 /\ B) is closed by A8, A10;
A13: [#] (X | A) = A by PRE_TOPC:8;
A14: [#] (X | B) = B by PRE_TOPC:8;
h " C = (f " C) \/ (g " C) by A1, Th1
.= ((f " C) \/ (g " C)) /\ (A \/ B) by A13, A14, XBOOLE_1:13, XBOOLE_1:28 ;
hence h " C is closed by A12, A9, A11, A6, A13, A14, PRE_TOPC:13; :: thesis: verum

end;

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