let f1, f2, g1, g2 be complex-valued FinSequence; ( len f1 = len g1 & len f2 <= len g2 implies (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2) )
assume that
A1:
len f1 = len g1
and
A2:
len f2 <= len g2
; (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)
A3:
( dom f1 = Seg (len f1) & dom f2 = Seg (len f2) & dom g1 = Seg (len g1) & dom g2 = Seg (len g2) )
by FINSEQ_1:def 3;
A4:
( dom (f1 ^ f2) = Seg (len (f1 ^ f2)) & dom (g1 ^ g2) = Seg (len (g1 ^ g2)) )
by FINSEQ_1:def 3;
A5:
( len (f1 ^ f2) = (len f1) + (len f2) & len (g1 ^ g2) = (len g1) + (len g2) )
by FINSEQ_1:22;
then
(dom (f1 ^ f2)) /\ (dom (g1 ^ g2)) = dom (f1 ^ f2)
by A1, A2, XREAL_1:6, A4, FINSEQ_1:7;
then
dom ((f1 ^ f2) (#) (g1 ^ g2)) = dom (f1 ^ f2)
by VALUED_1:def 4;
then A6:
len ((f1 ^ f2) (#) (g1 ^ g2)) = len (f1 ^ f2)
by FINSEQ_3:29;
(dom f1) /\ (dom g1) = dom f1
by A1, A3;
then A7:
dom (f1 (#) g1) = dom f1
by VALUED_1:def 4;
then A8:
len (f1 (#) g1) = len f1
by FINSEQ_3:29;
A9:
(dom f2) /\ (dom g2) = dom f2
by A2, A3, FINSEQ_1:7;
then A10:
dom (f2 (#) g2) = dom f2
by VALUED_1:def 4;
then A11:
len (f2 (#) g2) = len f2
by FINSEQ_3:29;
for i being Nat st 1 <= i & i <= len (f1 ^ f2) holds
((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i
hence
(f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)
by A5, A6, A8, A11, FINSEQ_1:22; verum