theorem DOMN: :: NEWTON04:45

for a, b being Real
for n being Nat holds
( len ((a,b) In_Power n) = len (Newton_Coeff n) & len ((a,b) Subnomial n) = len (Newton_Coeff n) & len ((a,b) In_Power n) = len ((a,b) Subnomial n) & dom ((a,b) In_Power n) = dom (Newton_Coeff n) & dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) )