let n, k be Element of 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