theorem :: NEWTON04:73

for n being Nat
for a being Real holds Sum ((a,a) Subnomial n) = (Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power n))