theorem CONST: :: NEWTON04:60

for a being Real
for n, i being Nat st i in dom ((a,a) Subnomial n) holds
((a,a) Subnomial n) . i = a |^ n