let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for m, n being natural number holds (m + n) iter R = (m iter R) (#) (n iter R)
let R be RMembership_Func of X,X; :: thesis: for m, n being natural number holds (m + n) iter R = (m iter R) (#) (n iter R)
let m, n be natural number ; :: thesis: (m + n) iter R = (m iter R) (#) (n iter R)
defpred S₁[ natural number ] means (m + $1) iter R = (m iter R) (#) ($1 iter R);
(m iter R) (#) (0 iter R) = (m iter R) (#) (Imf X,X) by Th24
.= m iter R by Th23 ;
then A1: S₁[ 0 ] ;
A2: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: (m + n) iter R = (m iter R) (#) (n iter R) ; :: thesis: S₁[n + 1]
thus (m iter R) (#) ((n + 1) iter R) = (m iter R) (#) ((n iter R) (#) R) by Th26
.= ((m + n) iter R) (#) R by A3, LFUZZY_0:23
.= ((m + n) + 1) iter R by Th26
.= (m + (n + 1)) iter R ; :: thesis: verum

end;

for m being natural number holds S₁[m] from NAT_1:sch 2(A1, A2);
hence (m + n) iter R = (m iter R) (#) (n iter R) ; :: thesis: verum