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
A3: 0 + 1 <= m + 1 by XREAL_1:8;
thus 1 <= m + 1 by A3; :: thesis: verum

end;

deffunc H₂( Element of NAT ) -> 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();
A5: 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 );
A6: rseq . (0 + 1) = (0 + 1) ! by A4
.= (0 ! ) * 1 by NEWTON:21
.= 1 by NEWTON:18 ;
A7: S₁[ 0 ] by A4, A6, 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]
A10: 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 ;
thus S₁[l + 1] by A2, A9, A10, XREAL_1:153; :: thesis: verum

end;

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

end;

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