let a, b, c, d be Real; for n being Nat holds ((a * b),(c * d)) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
let n be Nat; ((a * b),(c * d)) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
( len (((a * b),(c * d)) Subnomial ((n + 1) - 1)) = len ((a,d) Subnomial ((n + 1) - 1)) & len (((a * b),(c * d)) Subnomial ((n + 1) - 1)) = len ((b,c) Subnomial ((n + 1) - 1)) )
;
then
( dom (((a * b),(c * d)) Subnomial n) = dom ((a,d) Subnomial n) & dom (((a * b),(c * d)) Subnomial n) = dom ((b,c) Subnomial n) )
by FINSEQ_3:29;
then A1:
dom (((a * b),(c * d)) Subnomial n) = (dom ((a,d) Subnomial n)) /\ (dom ((b,c) Subnomial n))
;
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)
by STT;
hence
((a * b),(c * d)) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
by A1, VALUED_1:def 4; verum