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