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 H₂( Nat) -> set = $1 ! ;
consider rseq being Real_Sequence such that
A3: for l being Nat holds rseq . l = H₂(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 S₁[ 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: S₁[ 0 ] by A3, NEWTON:12;
A5: for l being Nat st S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A6: ( rseq . l <= rseq . (l + 1) & rseq . l > 0 ) ; :: thesis: S₁[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 S₁[l + 1] by A2, A6, XREAL_1:151; :: thesis: verum

end;

for l being Nat holds S₁[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