let n be Element of NAT ; :: thesis: ( n > 0 implies ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) )
assume A1: n > 0 ; :: thesis: ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )
A2: len (1,(1 / n) In_Power n) = n + 1 by NEWTON:def 4;

A3: now

let k be Element of NAT ; :: thesis: ( k < n + 1 implies (cseq n) . k = (1,(1 / n) In_Power n) . (k + 1) )
assume k < n + 1 ; :: thesis: (cseq n) . k = (1,(1 / n) In_Power n) . (k + 1)
then k <= n by NAT_1:13;
hence (cseq n) . k = (1,(1 / n) In_Power n) . (k + 1) by A1, Th21; :: thesis: verum

end;

A4: now

let k be Element of NAT ; :: thesis: ( k >= n + 1 implies (cseq n) . k = 0 )
assume k >= n + 1 ; :: thesis: (cseq n) . k = 0
then A5: k > n by NAT_1:13;
thus (cseq n) . k = (n choose k) * (n ^ (- k)) by Def3
.= 0 * (n ^ (- k)) by A5, NEWTON:def 3
.= 0 ; :: thesis: verum

end;

hence cseq n is summable by A2, A3, Th19; :: thesis: ( Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )
thus (1 + (1 / n)) ^ n = Sum (1,(1 / n) In_Power n) by NEWTON:41
.= Sum (cseq n) by A2, A3, A4, Th19 ; :: thesis: Sum (cseq n) = dseq . n
hence Sum (cseq n) = dseq . n by Def4; :: thesis: verum