let n, k be Element of NAT ; :: thesis: ( n <= k implies n ! <= k ! )
assume A1: n <= k ; :: thesis: n ! <= k !
A2: for m being Element of NAT holds 1 <= m + 1

proof

let m be Element of NAT ; :: thesis: 1 <= m + 1
0 + 1 <= m + 1 by XREAL_1:8;
hence 1 <= m + 1 ; :: thesis: verum

end;

deffunc H₂( Element of NAT ) -> Element of REAL = $1 ! ;
consider rseq being Real_Sequence such that
A4: for l being Element of NAT holds rseq . l = H₂(l) from SEQ_1:sch 1();
for l being Element of NAT holds
( rseq . l <= rseq . (l + 1) & rseq . l > 0 )

proof

let l be Element of NAT ; :: thesis: ( rseq . l <= rseq . (l + 1) & rseq . l > 0 )
defpred S₁[ Element of NAT ] means ( rseq . $1 <= rseq . ($1 + 1) & rseq . $1 > 0 );
rseq . (0 + 1) = (0 + 1) ! by A4
.= (0 ! ) * 1 by NEWTON:21
.= 1 by NEWTON:18 ;
then A7: S₁[ 0 ] by A4, NEWTON:18;
A8: for l being Element of NAT st S₁[l] holds
S₁[l + 1]

proof

let l be Element of NAT ; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A9: ( rseq . l <= rseq . (l + 1) & rseq . l > 0 ) ; :: thesis: S₁[l + 1]
rseq . ((l + 1) + 1) = ((l + 1) + 1) ! by A4
.= ((l + 1) ! ) * ((l + 1) + 1) by NEWTON:21
.= (rseq . (l + 1)) * ((l + 1) + 1) by A4 ;
hence S₁[l + 1] by A2, A9, XREAL_1:153; :: thesis: verum

end;

for l being Element of NAT holds S₁[l] from NAT_1:sch 1(A7, A8);
hence ( rseq . l <= rseq . (l + 1) & rseq . l > 0 ) ; :: thesis: verum

end;

then A12: rseq is non-decreasing by SEQM_3:def 13;
( n ! = rseq . n & k ! = rseq . k ) by A4;
hence n ! <= k ! by A1, A12, SEQM_3:12; :: thesis: verum