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
A13: 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
A14: 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 A15: [a,b] in IT1 ; :: thesis: [a,b] in IT2
then A16: ( 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 A13, A15;
hence [a,b] in IT2 by A14, A16; :: thesis: verum

end;

assume A17: [a,b] in IT2 ; :: thesis: [a,b] in IT1
then A18: ( 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, A17;
hence [a,b] in IT1 by A13, A18; :: thesis: verum