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)
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (f +* g) " A or x in (f " A) \/ (g " A) )
assume x in (f +* g) " A ; :: thesis: x in (f " A) \/ (g " A)
then A2: ( x in dom (f +* g) & (f +* g) . x in A ) by FUNCT_1:def 13;
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 ( ( x in dom f & (f +* g) . x = f . x ) or ( x in dom g & (f +* g) . x = g . x ) ) by A1, FUNCT_4:14, FUNCT_4:16;
then ( x in f " A or x in g " A ) by A2, FUNCT_1:def 13;
hence x in (f " A) \/ (g " A) by XBOOLE_0:def 3; :: thesis: verum

end;

( f c= f +* g & g c= f +* g ) by A1, FUNCT_4:26, FUNCT_4:29;
then ( f " A c= (f +* g) " A & g " A c= (f +* g) " A ) by RELAT_1:179;
hence (f " A) \/ (g " A) c= (f +* g) " A by XBOOLE_1:8; :: thesis: verum