let n be Nat; :: thesis: ( n > 0 implies ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n ) )

A1: now :: thesis: for k being Nat st k >= n + 1 holds
(cseq n) . k = 0

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

end;

assume A3: n > 0 ; :: thesis: ( cseq n is summable & Sum (cseq n) = (1 + (1 / n)) ^ n & Sum (cseq n) = dseq . n )

A4: now :: thesis: for k being Nat st k < n + 1 holds
(cseq n) . k = ((1,(1 / n)) In_Power n) . (k + 1)

let k be 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 A3, Th20; :: thesis: verum

end;

A5: len ((1,(1 / n)) In_Power n) = n + 1 by NEWTON:def 4;
hence cseq n is summable by A4, A1, Th18; :: 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:30
.= Sum (cseq n) by A5, A4, A1, Th18 ; :: thesis: Sum (cseq n) = dseq . n
hence Sum (cseq n) = dseq . n by Def4; :: thesis: verum