let f, g be Function; :: thesis: ( f tolerates g implies for A being set holds (f +* g) " A = (f " A) \/ (g " A) )
assume A1: f tolerates g ; :: thesis: for A being set holds (f +* g) " A = (f " A) \/ (g " A)
let A be set ; :: thesis: (f +* g) " A = (f " A) \/ (g " A)
f c= f +* g by A1, FUNCT_4:28;
then A2: f " A c= (f +* g) " A by RELAT_1:144;
thus (f +* g) " A c= (f " A) \/ (g " A) :: according to XBOOLE_0:def 10 :: thesis: (f " A) \/ (g " A) c= (f +* g) " A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f +* g) " A or x in (f " A) \/ (g " A) )
assume A3: x in (f +* g) " A ; :: thesis: x in (f " A) \/ (g " A)
then x in dom (f +* g) by FUNCT_1:def 7;
then x in (dom f) \/ (dom g) by FUNCT_4:def 1;
then ( x in dom f or x in dom g ) by XBOOLE_0:def 3;
then A4: ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by A1, FUNCT_4:13, FUNCT_4:15;
(f +* g) . x in A by A3, FUNCT_1:def 7;
then ( x in f " A or x in g " A ) by A4, FUNCT_1:def 7;
hence x in (f " A) \/ (g " A) by XBOOLE_0:def 3; :: thesis: verum

end;

g " A c= (f +* g) " A by FUNCT_4:25, RELAT_1:144;
hence (f " A) \/ (g " A) c= (f +* g) " A by A2, XBOOLE_1:8; :: thesis: verum