let a, b, c, d be Real; :: thesis: for n being Nat holds ((a * b),(c * d)) In_Power n = ((Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n)
let n be Nat; :: thesis: ((a * b),(c * d)) In_Power n = ((Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n)
((a * b),(c * d)) In_Power n = (Newton_Coeff n) (#) (((a * b),(c * d)) Subnomial n) by INS
.= (Newton_Coeff n) (#) (((a,c) Subnomial n) (#) ((b,d) Subnomial n)) by ST ;
hence ((a * b),(c * d)) In_Power n = ((Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n) by RFUNCT_1:9; :: thesis: verum