let n be Nat; :: thesis: for a being Real holds Sum ((a,a) Subnomial n) = (Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power n))
let a be Real; :: thesis: Sum ((a,a) Subnomial n) = (Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power n))
(Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power ((n + 1) - 1))) = (n + 1) * ((a + 0) |^ n) by NEWTON:30;
hence Sum ((a,a) Subnomial n) = (Sum ((1,1) Subnomial n)) * (Sum ((a,0) In_Power n)) by SAA; :: thesis: verum