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 (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 (n iter R)
let m, n be natural number ; :: thesis: (m * n) iter R = m iter (n iter R)
defpred S₁[ natural number ] means ($1 * n) iter R = $1 iter (n iter R);
(0 * n) iter R = Imf X,X by Th24
.= 0 iter (n iter R) by Th24 ;
then A1: S₁[ 0 ] ;
A2: for m being natural number st S₁[m] holds
S₁[m + 1]

proof

let m be natural number ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A3: (m * n) iter R = m iter (n iter R) ; :: thesis: S₁[m + 1]
A4: ((m + 1) * n) iter R = ((m * n) + (1 * n)) iter R
.= (m iter (n iter R)) (#) (n iter R) by A3, Th27 ;
(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 ;
hence S₁[m + 1] by A4; :: 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 (n iter R) ; :: thesis: verum