theorem CONST1: :: NEWTON04:61

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