:: deftheorem Def9 defines iter LFUZZY_1:def 9 :
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat
for b₄ being RMembership_Func of X,X holds
( b₄ = n iter R iff ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st
( b₄ = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) );