let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds 1 iter R = R
let R be RMembership_Func of X,X; :: thesis: 1 iter R = R
consider F being sequence of (Funcs ([:X,X:],[.0,1.])) such that
A1: ( 1 iter R = F . 1 & F . 0 = Imf (X,X) ) and
A2: for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) by Def9;
ex Q being RMembership_Func of X,X st
( F . 0 = Q & F . (0 + 1) = Q (#) R ) by A2;
hence 1 iter R = R by A1, Th22; :: thesis: verum