theorem Th20: :: IRRAT_1:20

for k, n being Nat st n > 0 & k <= n holds
(cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1)