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