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 )

f /. c = g /. c ; :: thesis: f tolerates g

( 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 A5:
for c being Element of C st c in (dom f) /\ (dom g) holds
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;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

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

hence
f tolerates g
by PARTFUN1:def 4; :: thesis: verumf . 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;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