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