theorem Th2: :: HILB10_5:2

for n, m being Nat st m >= n & n > 0 holds
1 + ((m !) * (idseq n)) is CR_Sequence