let m be Nat; :: thesis: for f being Function holds iter (f,(m + 1)) c= f [*]
let f be Function; :: thesis: iter (f,(m + 1)) c= f [*]
set RH = f [*] ;
defpred S₁[ Nat] means iter (f,($1 + 1)) c= f [*] ;
A1: S₁[ 0 ]

proof

A2: iter (f,1) = f by FUNCT_7:70;
thus S₁[ 0 ] by LANG1:18, A2; :: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then ( iter (f,(n + 1)) c= f [*] & f c= f [*] ) by LANG1:18;
then A4: (iter (f,(n + 1))) * f c= (f [*]) * (f [*]) by RELAT_1:31;
(f [*]) * (f [*]) c= f [*] by RELAT_2:27;
then (iter (f,(n + 1))) * f c= f [*] by A4;
hence S₁[n + 1] by FUNCT_7:69; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence iter (f,(m + 1)) c= f [*] ; :: thesis: verum