let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for n being natural number holds (n + 1) iter R = (n iter R) (#) R
let R be RMembership_Func of X,X; :: thesis: for n being natural number holds (n + 1) iter R = (n iter R) (#) R
let n be natural number ; :: thesis: (n + 1) iter R = (n iter R) (#) R
consider f being Function of NAT ,(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 natural number ex Q being RMembership_Func of X,X st
( f . k = Q & f . (k + 1) = Q (#) R ) by Def10;
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, Def10; :: thesis: verum