let f be Function; :: thesis: for m, n being Element of NAT st rng f c= dom f holds
iter ((iter (f,m)),n) = iter (f,(m * n))
let m, n be Element of NAT ; :: thesis: ( rng f c= dom f implies iter ((iter (f,m)),n) = iter (f,(m * n)) )
defpred S₁[ Element of NAT ] means iter ((iter (f,m)),$1) = iter (f,(m * $1));
assume A1: rng f c= dom f ; :: thesis: iter ((iter (f,m)),n) = iter (f,(m * n))
then dom (iter (f,m)) = dom f by Th76;
then (dom (iter (f,m))) \/ (rng (iter (f,m))) = dom f by A1, Th76, XBOOLE_1:12;
then iter ((iter (f,m)),0) = id (dom f) by Th70
.= id ((dom f) \/ (rng f)) by A1, XBOOLE_1:12
.= iter (f,(m * 0)) by Th70 ;
then A2: S₁[ 0 ] ;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1] by Lm5;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
hence iter ((iter (f,m)),n) = iter (f,(m * n)) ; :: thesis: verum