let m, n be Nat; :: thesis: for R being Relation st n <> 0 holds
iter ((iter (R,m)),n) = iter (R,(m * n))
let R be Relation; :: thesis: ( n <> 0 implies iter ((iter (R,m)),n) = iter (R,(m * n)) )
defpred S₁[ Nat] means iter ((iter (R,m)),($1 + 1)) = iter (R,(m * ($1 + 1)));
A1: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm5;
A2: S₁[ 0 ] by Th69;
A3: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
assume n <> 0 ; :: thesis: iter ((iter (R,m)),n) = iter (R,(m * n))
then consider k being Nat such that
A4: n = k + 1 by NAT_1:6;
reconsider k = k as Nat ;
n = k + 1 by A4;
hence iter ((iter (R,m)),n) = iter (R,(m * n)) by A3; :: thesis: verum