for a, b, c, d being Real
for n being Nat holds ((a * b),(c * d)) In_Power n = ((Newton_Coeff n) (#) ((a,c) Subnomial n)) (#) ((b,d) Subnomial n)