consider p being sequence of (bool [:(field f),(field f):]) such that
A1: ( p . n = iter (f,n) & p . 0 = id (field f) ) and
A2: for k being Nat holds p . (k + 1) = f * (p . k) by Def10;
defpred S₁[ Nat] means p . f is Function;
A3: S₁[ 0 ] by A1;
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 Function ;
p . (m + 1) = g * f 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 (f,n) is Function-like by A1; :: thesis: verum