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 S₁[ Nat] means ($1 * n) iter R = $1 iter (n iter R);
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: (m * n) iter R = m iter (n iter R) ; :: thesis: S₁[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 A2, Th27 ;
hence S₁[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: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A4, A1);
hence (m * n) iter R = m iter (n iter R) ; :: thesis: verum