let C, D be non empty set ; :: thesis: for f, g being PartFunc of C,D holds
( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )
let f, g be PartFunc of C,D; :: thesis: ( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )
thus ( f tolerates g implies for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ) :: thesis: ( ( for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ) implies f tolerates g )

proof

assume A1: f tolerates g ; :: thesis: for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c
let c be Element of C; :: thesis: ( c in (dom f) /\ (dom g) implies f /. c = g /. c )
assume A2: c in (dom f) /\ (dom g) ; :: thesis: f /. c = g /. c
then A3: c in dom f by XBOOLE_0:def 4;
f . c = g . c by A1, A2, PARTFUN1:def 4;
then A4: f /. c = g . c by A3, PARTFUN1:def 6;
c in dom g by A2, XBOOLE_0:def 4;
hence f /. c = g /. c by A4, PARTFUN1:def 6; :: thesis: verum

end;

assume A5: for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c ; :: thesis: f tolerates g

now :: thesis: for x being object st x in (dom f) /\ (dom g) holds
f . x = g . x

let x be object ; :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A6: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then reconsider x1 = x as Element of C ;
( x in dom f & f /. x1 = g /. x1 ) by A5, A6, XBOOLE_0:def 4;
then A7: f . x = g /. x1 by PARTFUN1:def 6;
x in dom g by A6, XBOOLE_0:def 4;
hence f . x = g . x by A7, PARTFUN1:def 6; :: thesis: verum

end;

hence f tolerates g by PARTFUN1:def 4; :: thesis: verum