let a, b, c, d be Real; :: thesis: for n being Nat holds ((a * b),(c * d)) Subnomial n = ((a,d) Subnomial n) (#) ((b,c) Subnomial n)
let n be Nat; :: thesis: ((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; :: thesis: verum