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)

ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( 0 iter R = F . 0 & 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 ) ) ) by Def9;

hence 0 iter R = Imf (X,X) ; :: thesis: verum

let R be RMembership_Func of X,X; :: thesis: 0 iter R = Imf (X,X)

ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( 0 iter R = F . 0 & 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 ) ) ) by Def9;

hence 0 iter R = Imf (X,X) ; :: thesis: verum