:: deftheorem Def7 defines =_ ABIAN:def 7 :
for E being set
for f being Function of E,E
for b₃ being Equivalence_Relation of E holds
( b₃ = =_ f iff for x, y being set st x in E & y in E holds
( [x,y] in b₃ iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y ) );