let X be non empty set ; :: thesis: for R being RMembership_Func of X,X
for m, n being Nat holds (m * n) iter R = m iter (n iter R)

let R be RMembership_Func of X,X; :: thesis: for m, n being Nat holds (m * n) iter R = m iter (n iter R)
let m, n be Nat; :: thesis: (m * n) iter R = m iter (n iter R)
defpred S1[ Nat] means (\$1 * n) iter R = \$1 iter (n iter R);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A2: (m * n) iter R = m iter (n iter R) ; :: thesis: S1[m + 1]
A3: (m + 1) iter (n iter R) = (m iter (n iter R)) (#) (1 iter (n iter R)) by Th27
.= (m iter (n iter R)) (#) (n iter R) by Th25 ;
((m + 1) * n) iter R = ((m * n) + (1 * n)) iter R
.= (m iter (n iter R)) (#) (n iter R) by ;
hence S1[m + 1] by A3; :: thesis: verum
end;
(0 * n) iter R = Imf (X,X) by Th24
.= 0 iter (n iter R) by Th24 ;
then A4: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A4, A1);
hence (m * n) iter R = m iter (n iter R) ; :: thesis: verum