let IT1, IT2 be Equivalence_Relation of E; :: thesis: ( ( for x, y being set st x in E & y in E holds
( [x,y] in IT1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) & ( for x, y being set st x in E & y in E holds
( [x,y] in IT2 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ) implies IT1 = IT2 )
assume that
A14: for x, y being set st x in E & y in E holds
( [x,y] in IT1 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) and
A15: for x, y being set st x in E & y in E holds
( [x,y] in IT2 iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) ; :: thesis: IT1 = IT2
let a, b be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [a,b] in IT1 or [a,b] in IT2 ) & ( not [a,b] in IT2 or [a,b] in IT1 ) )

hereby :: thesis: ( not [a,b] in IT2 or [a,b] in IT1 )

assume A16: [a,b] in IT1 ; :: thesis: [a,b] in IT2
then A17: ( a in E & b in E ) by ZFMISC_1:106;
then ex k, l being Element of NAT st (iter f,k) . a = (iter f,l) . b by A14, A16;
hence [a,b] in IT2 by A15, A17; :: thesis: verum

end;

assume A18: [a,b] in IT2 ; :: thesis: [a,b] in IT1
then A19: ( a in E & b in E ) by ZFMISC_1:106;
then ex k, l being Element of NAT st (iter f,k) . a = (iter f,l) . b by A15, A18;
hence [a,b] in IT1 by A14, A19; :: thesis: verum