theorem :: NEWTON04:93

for a, b being Real
for n being Nat holds (a,b) Subnomial (n + 2) = (<*(a |^ (n + 2))*> ^ ((a * b) * ((a,b) Subnomial n))) ^ <*(b |^ (n + 2))*>