theorem Th14: :: IRRAT_1:14

for k, n being Nat st n > 0 holds
( 0 <= (bseq k) . n & (bseq k) . n <= 1 / (k !) & (bseq k) . n <= eseq . k & 0 <= (cseq n) . k & (cseq n) . k <= 1 / (k !) & (cseq n) . k <= eseq . k )