let m, n be Nat; :: thesis: for R being Relation st rng R c= dom R holds
iter ((iter (R,m)),n) = iter (R,(m * n))
let R be Relation; :: thesis: ( rng R c= dom R implies iter ((iter (R,m)),n) = iter (R,(m * n)) )
defpred S₁[ Nat] means iter ((iter (R,m)),$1) = iter (R,(m * $1));
assume A1: rng R c= dom R ; :: thesis: iter ((iter (R,m)),n) = iter (R,(m * n))
then dom (iter (R,m)) = dom R by Th73;
then field (iter (R,m)) = dom R by A1, Th73, XBOOLE_1:12;
then iter ((iter (R,m)),0) = id (dom R) by Th67
.= id (field R) by A1, XBOOLE_1:12
.= iter (R,(m * 0)) by Th67 ;
then A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm5;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
hence iter ((iter (R,m)),n) = iter (R,(m * n)) ; :: thesis: verum