for a, b, c, d being Real
for n being Nat
for x being object st x in dom (((a * b),(c * d)) Subnomial n) holds
(((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)