let k, n be Nat; :: thesis: (cseq n) . k = (bseq k) . n
thus (cseq n) . k = (n choose k) * (n ^ (- k)) by Def3
.= (bseq k) . n by Def2 ; :: thesis: verum