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