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

A1: now

let n be Element of 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 Th73
.= compose (((n |-> f) ^ <*f*>),(field f)) by Th43
.= compose (((n + 1) |-> f),(field f)) by FINSEQ_2:60 ;
hence S₁[n + 1] ; :: thesis: verum

end;

iter (f,0) = id (field f) by Th70
.= compose ({},(field f)) by Th41
.= compose ((0 |-> f),(field f)) ;
then A2: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum