theorem SAN: :: NEWTON04:92

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