let a, b be 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) )
let n be Nat; ( ((a,b) In_Power n) . 1 = ((a,b) Subnomial n) . 1 & ((a,b) In_Power n) . (n + 1) = ((a,b) Subnomial n) . (n + 1) )
A1:
((a,b) Subnomial n) . 1 = (((a,b) In_Power n) . 1) / ((Newton_Coeff n) . 1)
by VALUED_1:17;
((a,b) Subnomial n) . (n + 1) = (((a,b) In_Power n) . (n + 1)) / ((Newton_Coeff n) . (n + 1))
by VALUED_1:17;
hence
( ((a,b) In_Power n) . 1 = ((a,b) Subnomial n) . 1 & ((a,b) In_Power n) . (n + 1) = ((a,b) Subnomial n) . (n + 1) )
by A1; verum