let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being Nat holds (n + 1) iter R = (n iter R) (#) R
let R be RMembership_Func of X,X; :: thesis: for n being Nat holds (n + 1) iter R = (n iter R) (#) R
let n be Nat; :: thesis: (n + 1) iter R = (n iter R) (#) R
consider f being sequence of (Funcs ([:X,X:],[.0,1.])) such that
A1: ( (n + 1) iter R = f . (n + 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 . n = Q & f . (n + 1) = Q (#) R ) by A2;
hence (n + 1) iter R = (n iter R) (#) R by A1, A2, Def9; :: thesis: verum