let a be Real; for n being Nat holds Sum ((a,a) Subnomial n) = (n + 1) * (a |^ n)
let n be Nat; 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; verum