let f, g be Function; :: thesis: ( f tolerates g iff f +* g = g +* f )
thus ( f tolerates g implies f +* g = g +* f ) :: thesis: ( f +* g = g +* f implies f tolerates g )

proof

assume A1: f tolerates g ; :: thesis: f +* g = g +* f
A2: dom (f +* g) = (dom g) \/ (dom f) by Def1
.= dom (g +* f) by Def1 ;
for x being set st x in dom (f +* g) holds
(f +* g) . x = (g +* f) . x

proof

let x be set ; :: thesis: ( x in dom (f +* g) implies (f +* g) . x = (g +* f) . x )
assume A3: x in dom (f +* g) ; :: thesis: (f +* g) . x = (g +* f) . x

now

A4: dom (f +* g) = (dom f) \/ (dom g) by Def1;

per cases ( ( x in dom f & x in dom g ) or ( x in dom f & not x in dom g ) or ( not x in dom f & x in dom g ) ) by A3, A4, XBOOLE_0:def 3;

suppose ( x in dom f & x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x

then ( x in (dom f) /\ (dom g) & (f +* g) . x = g . x & (g +* f) . x = f . x ) by Th14, XBOOLE_0:def 4;
hence (f +* g) . x = (g +* f) . x by A1, PARTFUN1:def 6; :: thesis: verum

end;

suppose ( x in dom f & not x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x

then ( (f +* g) . x = f . x & (g +* f) . x = f . x ) by Th12, Th14;
hence (f +* g) . x = (g +* f) . x ; :: thesis: verum

end;

suppose ( not x in dom f & x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x

then ( (f +* g) . x = g . x & (g +* f) . x = g . x ) by Th12, Th14;
hence (f +* g) . x = (g +* f) . x ; :: thesis: verum

end;

end;

end;

hence (f +* g) . x = (g +* f) . x ; :: thesis: verum

end;

hence f +* g = g +* f by A2, FUNCT_1:9; :: thesis: verum

end;

assume A5: f +* g = g +* f ; :: thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( (f +* g) . x = g . x & (g +* f) . x = f . x ) by Th14;
hence f . x = g . x by A5; :: thesis: verum