let R be Relation; for n being Nat holds iter (R,(n + 1)) = (iter (R,n)) * R
let n be Nat; iter (R,(n + 1)) = (iter (R,n)) * R
defpred S1[ Nat] means iter (R,($1 + 1)) = (iter (R,$1)) * R;
A1:
for k being Nat st S1[k] holds
S1[k + 1]
iter (R,(0 + 1)) =
R
by Th69
.=
(id (field R)) * R
by Lm3
.=
(iter (R,0)) * R
by Th67
;
then A3:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A3, A1);
hence
iter (R,(n + 1)) = (iter (R,n)) * R
; verum