let m, n be Nat; :: thesis: for R being Relation holds (iter (R,m)) * (iter (R,n)) = iter (R,(n + m))
let R be Relation; :: thesis: (iter (R,m)) * (iter (R,n)) = iter (R,(n + m))
defpred S₁[ Nat] means (iter (R,$1)) * (iter (R,n)) = iter (R,(n + $1));
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: (iter (R,k)) * (iter (R,n)) = iter (R,(n + k)) ; :: thesis: S₁[k + 1]
thus (iter (R,(k + 1))) * (iter (R,n)) = (R * (iter (R,k))) * (iter (R,n)) by Th68
.= R * ((iter (R,k)) * (iter (R,n))) by RELAT_1:36
.= iter (R,((n + k) + 1)) by A2, Th68
.= iter (R,(n + (k + 1))) ; :: thesis: verum

end;

(iter (R,0)) * (iter (R,n)) = (id (field R)) * (iter (R,n)) by Th67
.= iter (R,(n + 0)) by Th74 ;
then A3: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A1);
hence (iter (R,m)) * (iter (R,n)) = iter (R,(n + m)) ; :: thesis: verum