let X be non empty set ; :: thesis: for R being RMembership_Func of X,X holds 0 iter R = Imf X,X
let R be RMembership_Func of X,X; :: thesis: 0 iter R = Imf X,X
consider F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) such that
A1: ( 0 iter R = F . 0 & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) by Def10;
thus 0 iter R = Imf X,X by A1; :: thesis: verum