let k, n be Nat; :: thesis: ( n <= k implies n ! <= k ! )
assume A1: n <= k ; :: thesis: n ! <= k !
A2: for m being Nat holds 1 <= m + 1
proof
let m be Nat; :: thesis: 1 <= m + 1
0 + 1 <= m + 1 by XREAL_1:6;
hence 1 <= m + 1 ; :: thesis: verum
end;
deffunc H2( Nat) -> set = $1 ! ;
consider rseq being Real_Sequence such that
A3: for l being Nat holds rseq . l = H2(l) from SEQ_1:sch 1();
 for l being Nat holds
( rseq . l <= rseq . (l + 1) & rseq . l > 0 )
proof
let l be Nat; :: thesis: ( rseq . l <= rseq . (l + 1) & rseq . l > 0 )
defpred S1[ Nat] means ( rseq . $1 <= rseq . ($1 + 1) & rseq . $1 > 0 );
rseq . (0 + 1) = (0 + 1) ! by A3
.= (0 !) * 1 by NEWTON:15
.= 1 by NEWTON:12 ;
then A4: S1[ 0 ] by A3, NEWTON:12;
A5: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume A6: ( rseq . l <= rseq . (l + 1) & rseq . l > 0 ) ; :: thesis: S1[l + 1]
rseq . ((l + 1) + 1) = ((l + 1) + 1) ! by A3
.= ((l + 1) !) * ((l + 1) + 1) by NEWTON:15
.= (rseq . (l + 1)) * ((l + 1) + 1) by A3 ;
hence S1[l + 1] by A2, A6, XREAL_1:151; :: thesis: verum
end;
for l being Nat holds S1[l] from NAT_1:sch 2(A4, A5);
 hence ( rseq . l <= rseq . (l + 1) & rseq . l > 0 ) ; :: thesis: verum
end;
then A7: rseq is non-decreasing ;
( n ! = rseq . n & k ! = rseq . k ) by A3;
hence n ! <= k ! by A1, A7, SEQM_3:6; :: thesis: verum