let a, b be Real; :: thesis: for n being Nat holds
( (a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) & (a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n) )
let n be Nat; :: thesis: ( (a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) & (a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n) )
A1: (a,b) In_Power n = (Newton_Coeff n) (#) ((a,b) Subnomial n) by INS
.= (Newton_Coeff n) (#) (((a,1) Subnomial n) (#) ((1,b) Subnomial n)) by DAB ;
( (Newton_Coeff n) (#) ((a,1) Subnomial n) = (a,1) In_Power n & (Newton_Coeff n) (#) ((1,b) Subnomial n) = (1,b) In_Power n ) by INS;
hence ( (a,b) In_Power n = ((a,1) In_Power n) (#) ((1,b) Subnomial n) & (a,b) In_Power n = ((a,1) Subnomial n) (#) ((1,b) In_Power n) ) by A1, F123; :: thesis: verum