consider p being Function of NAT,(bool [:(field R),(field R):]) such that
A1: ( p . n = iter (R,n) & p . 0 = id (field R) ) and
A2: for k being Nat holds p . (k + 1) = R * (p . k) by FUNCT_7:def 11;
defpred S₁[ Nat] means p . $1 is Relation of X;
field R c= X \/ X by RELSET_1:8;
then ( dom (id (field R)) c= X & rng (id (field R)) c= X ) ;
then A3: S₁[ 0 ] by A1, RELSET_1:4;
A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then reconsider g = p . m as Relation of X ;
p . (m + 1) = R * g by A2;
hence S₁[m + 1] ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A4);
hence iter (R,n) is Relation of X by A1; :: thesis: verum