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 S1[ Nat] means iter (f,($1 + 1)) c= f [*] ;
A1: S1[ 0 ]
proof
A2: iter (f,1) = f by FUNCT_7:70;
thus S1[ 0 ] by LANG1:18, A2; :: thesis: verum
end;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[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 S1[n + 1] by FUNCT_7:69; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A1, A3);
 hence iter (f,(m + 1)) c= f [*] ; :: thesis: verum