theorem Th3: :: IRRAT_1:3

for k, n being Nat holds (cseq n) . k = (bseq k) . n