let R be Relation; :: thesis: for n being Nat holds iter (R,(n + 1)) = (iter (R,n)) * R
let n be Nat; :: thesis: iter (R,(n + 1)) = (iter (R,n)) * R
defpred S₁[ Nat] means iter (R,($1 + 1)) = (iter (R,$1)) * R;
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 + 1)) = (iter (R,k)) * R ; :: thesis: S₁[k + 1]
thus (iter (R,(k + 1))) * R = (R * (iter (R,k))) * R by Th68
.= R * ((iter (R,k)) * R) by RELAT_1:36
.= iter (R,((k + 1) + 1)) by A2, Th68 ; :: thesis: verum

end;

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