let f be Function; :: thesis: for n being Element of NAT holds iter (f,n) = compose ((n |-> f),((dom f) \/ (rng f)))
defpred S₁[ Element of NAT ] means iter (f,$1) = compose (($1 |-> f),((dom f) \/ (rng 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),((dom f) \/ (rng f)))) by Th73
.= compose (((n |-> f) ^ <*f*>),((dom f) \/ (rng f))) by Th43
.= compose (((n + 1) |-> f),((dom f) \/ (rng f))) by FINSEQ_2:74 ;
hence S₁[n + 1] ; :: thesis: verum

end;

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