let m, n be Element of 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₁[ Element of NAT ] means (iter (R,$1)) * (iter (R,n)) = iter (R,(n + $1));
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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 Th71
.= R * ((iter (R,k)) * (iter (R,n))) by RELAT_1:36
.= iter (R,((n + k) + 1)) by A2, Th71
.= iter (R,(n + (k + 1))) ; :: thesis: verum

end;

(iter (R,0)) * (iter (R,n)) = (id (field R)) * (iter (R,n)) by Th70
.= iter (R,(n + 0)) by Th77 ;
then A3: S₁[ 0 ] ;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A1);
hence (iter (R,m)) * (iter (R,n)) = iter (R,(n + m)) ; :: thesis: verum