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 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 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 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 Nat st (iter (f,k)) . x = (iter (f,l)) . y ) ; :: thesis: IT1 = IT2
let a, b be object ; :: 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:87;
then ex k, l being 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:87;
then ex k, l being Nat st (iter (f,k)) . a = (iter (f,l)) . b by A15, A18;
hence [a,b] in IT1 by A14, A19; :: thesis: verum