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

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