let a be Real; :: thesis: for n being Nat holds Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n)
let n be Nat; :: thesis: Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n)
A1: n + 1 = len ((a,a) Subnomial ((n + 1) - 1)) ;
n + 1 >= 0 + 1 by XREAL_1:6;
then A2: n + 1 in dom ((a,a) Subnomial n) by A1, FINSEQ_3:25;
( n + 1 is set & n + 1 in dom ((a,a) Subnomial n) & ((a,a) Subnomial n) . (n + 1) = a |^ n ) by A2, CONST;
then the_value_of ((a,a) Subnomial n) = a |^ n by FUNCT_1:def 12;
hence Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n) by A1, RVSUM_3:7; :: thesis: verum