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: for x being object st x in dom (f +* g) holds
(f +* g) . x = (g +* f) . x
proof
let x be object ; :: 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 :: thesis: (f +* g) . x = (g +* f) . x
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 A5: ( x in dom f & x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x
then A6: (g +* f) . x = f . x by Th13;
( x in (dom f) /\ (dom g) & (f +* g) . x = g . x ) by A5, Th13, XBOOLE_0:def 4;
hence (f +* g) . x = (g +* f) . x by A1, A6; :: thesis: verum
end;
suppose A7: ( x in dom f & not x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x
then (f +* g) . x = f . x by Th11;
hence (f +* g) . x = (g +* f) . x by A7, Th13; :: thesis: verum
end;
suppose A8: ( not x in dom f & x in dom g ) ; :: thesis: (f +* g) . x = (g +* f) . x
then (f +* g) . x = g . x by Th13;
hence (f +* g) . x = (g +* f) . x by A8, Th11; :: thesis: verum
end;
end;
end;
hence (f +* g) . x = (g +* f) . x ; :: thesis: verum
end;
dom (f +* g) = (dom g) \/ (dom f) by Def1
.= dom (g +* f) by Def1 ;
hence f +* g = g +* f by A2; :: thesis: verum
end;
assume A9: f +* g = g +* f ; :: thesis: f tolerates g
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( not x in (dom f) /\ (dom g) or f . x = g . x )
assume A10: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then x in dom g by XBOOLE_0:def 4;
then A11: (f +* g) . x = g . x by Th13;
x in dom f by A10, XBOOLE_0:def 4;
hence f . x = g . x by A9, A11, Th13; :: thesis: verum