let f, g be Function; :: thesis: ( g is f -tolerating iff for x being object st x in dom f & x in dom g holds

f . x = g . x )

thus ( g is f -tolerating implies for x being object st x in dom f & x in dom g holds

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

f . x = g . x ) implies g is f -tolerating )

f . x = g . x ; :: thesis: g is f -tolerating

let x be object ; :: according to PARTFUN1:def 4,AOFA_L00:def 1 :: 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;

hence f . x = g . x by A2; :: thesis: verum

f . x = g . x )

thus ( g is f -tolerating implies for x being object st x in dom f & x in dom g holds

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

f . x = g . x ) implies g is f -tolerating )

proof

assume A2:
for x being object st x in dom f & x in dom g holds
assume A1:
for x being object st x in (dom f) /\ (dom g) holds

f . x = g . x ; :: according to PARTFUN1:def 4,AOFA_L00:def 1 :: thesis: for x being object st x in dom f & x in dom g holds

f . x = g . x

let x be object ; :: thesis: ( x in dom f & x in dom g implies f . x = g . x )

assume ( x in dom f & x in dom g ) ; :: thesis: f . x = g . x

then x in (dom f) /\ (dom g) by XBOOLE_0:def 4;

hence f . x = g . x by A1; :: thesis: verum

end;f . x = g . x ; :: according to PARTFUN1:def 4,AOFA_L00:def 1 :: thesis: for x being object st x in dom f & x in dom g holds

f . x = g . x

let x be object ; :: thesis: ( x in dom f & x in dom g implies f . x = g . x )

assume ( x in dom f & x in dom g ) ; :: thesis: f . x = g . x

then x in (dom f) /\ (dom g) by XBOOLE_0:def 4;

hence f . x = g . x by A1; :: thesis: verum

f . x = g . x ; :: thesis: g is f -tolerating

let x be object ; :: according to PARTFUN1:def 4,AOFA_L00:def 1 :: 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;

hence f . x = g . x by A2; :: thesis: verum