let a, b be Real; :: thesis: 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; :: thesis: ( ((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; :: thesis: verum