let n be Element of NAT ; :: thesis: iter {} ,n = {}
defpred S₁[ Element of NAT ] means iter {} ,$1 = {} ;
A1: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume iter {} ,k = {} ; :: thesis: S₁[k + 1]
thus iter {} ,(k + 1) = (iter {} ,k) * {} by Th71
.= {} ; :: thesis: verum

end;

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