for a, b being Real
for n being Nat holds
( ((a,b) In_Power n) . 1 = ((a,b) Subnomial n) . 1 & ((a,b) In_Power n) . (n + 1) = ((a,b) Subnomial n) . (n + 1) )