let k, n be Nat; :: thesis: ( n > 0 & k <= n implies (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1) )
assume that
A1: n > 0 and
A2: k <= n ; :: thesis: (cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1)
thus ((1,(1 / n)) In_Power n) . (k + 1) = ((n choose k) * (1 ^ (n - k))) * ((1 / n) ^ k) by A2, Th19
.= ((n choose k) * 1) * ((1 / n) ^ k) by POWER:26
.= (n choose k) * (n ^ (- k)) by A1, POWER:32
.= (cseq n) . k by Def3 ; :: thesis: verum