let f be Function; :: thesis: for n being Nat holds iter (f,n) = compose ((n |-> f),(field f))
defpred S₁[ Nat] means iter (f,$1) = compose (($1 |-> f),(field f));

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then iter (f,(n + 1)) = f * (compose ((n |-> f),(field f))) by Th70
.= compose (((n |-> f) ^ <*f*>),(field f)) by Th40
.= compose (((n + 1) |-> f),(field f)) by FINSEQ_2:60 ;
hence S₁[n + 1] ; :: thesis: verum

end;

iter (f,0) = id (field f) by Th67
.= compose ({},(field f)) by Th38
.= compose ((0 |-> f),(field f)) ;
then A2: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1); :: thesis: verum