let f1, f2, g1, g2 be complex-valued FinSequence; :: thesis: ( 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 ; :: thesis: (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

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (f1 ^ f2) implies ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i )
assume ( 1 <= i & i <= len (f1 ^ f2) ) ; :: thesis: ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i
then A12: i in dom (f1 ^ f2) by FINSEQ_3:25;

per cases ( i in dom f1 or not i in dom f1 ) ;

suppose A13: i in dom f1 ; :: thesis: ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i

then A14: ( (f1 ^ f2) . i = f1 . i & (g1 ^ g2) . i = g1 . i ) by A1, A3, FINSEQ_1:def 7;
((f1 (#) g1) ^ (f2 (#) g2)) . i = (f1 (#) g1) . i by A13, A7, FINSEQ_1:def 7
.= (f1 . i) * (g1 . i) by VALUED_1:5 ;
hence ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i by A14, VALUED_1:5; :: thesis: verum

end;

suppose not i in dom f1 ; :: thesis: ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i

then consider j being Nat such that
A15: ( j in dom f2 & i = (len f1) + j ) by A12, FINSEQ_1:25;
A16: ( (f1 ^ f2) . i = f2 . j & (g1 ^ g2) . i = g2 . j ) by A9, A15, A1, FINSEQ_1:def 7;
((f1 (#) g1) ^ (f2 (#) g2)) . i = (f2 (#) g2) . j by A15, A8, A10, FINSEQ_1:def 7
.= (f2 . j) * (g2 . j) by VALUED_1:5 ;
hence ((f1 ^ f2) (#) (g1 ^ g2)) . i = ((f1 (#) g1) ^ (f2 (#) g2)) . i by VALUED_1:5, A16; :: thesis: verum

end;

end;

end;

hence (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2) by A5, A6, A8, A11, FINSEQ_1:22; :: thesis: verum