let f be Function; :: thesis: for n, m being Element of NAT st n <> 0 holds
iter (iter f,m),n = iter f,(m * n)
let n, m be Element of NAT ; :: thesis: ( n <> 0 implies iter (iter f,m),n = iter f,(m * n) )
defpred S₁[ Element of NAT ] means iter (iter f,m),($1 + 1) = iter f,(m * ($1 + 1));
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by Lm5;
A2: S₁[ 0 ] by Th72;
A3: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A1);
assume n <> 0 ; :: thesis: iter (iter f,m),n = iter f,(m * n)
then consider k being Nat such that
A4: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
n = k + 1 by A4;
hence iter (iter f,m),n = iter f,(m * n) by A3; :: thesis: verum