:: deftheorem Def10 defines iter FUNCT_7:def 11 :
for f being Relation
for n being Nat
for b₃ being Relation holds
( b₃ = iter (f,n) iff ex p being sequence of (bool [:(field f),(field f):]) st
( b₃ = p . n & p . 0 = id (field f) & ( for k being Nat holds p . (k + 1) = f * (p . k) ) ) );