let a, b be Complex; :: thesis:
let n be Nat; :: thesis:
let f, g be n -element complex-valued FinSequence; :: thesis:
reconsider fa = f ^ <*a*> as n + 1 -element FinSequence of COMPLEX by NEWTON02:103;
reconsider gb = g ^ <*b*> as n + 1 -element FinSequence of COMPLEX by NEWTON02:103;
reconsider fg = f (#) g as n -element complex-valued FinSequence ;
A0: ( len f = n & len g = n & len fg = n ) by FINSEQ_3:153;
A1: ( len fa = n + 1 & len gb = n + 1 & len (fg ^ <*(a * b)*>) = n + 1 ) by FINSEQ_3:153;
A2: n + 1 = len (fa (#) gb) by FINSEQ_3:153;
then A3: ( dom (fa (#) gb) = Seg (n + 1) & dom ((f (#) g) ^ <*(a * b)*>) = Seg (n + 1) ) by A1, FINSEQ_1:def 3;
for k being object st k in dom (fa (#) gb) holds
(fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k

let k be object ; :: thesis:
assume B1: k in dom (fa (#) gb) ; :: thesis:
B2: (fa (#) gb) . k = (fa . k) * (gb . k) by B1, VALUED_1:def 4;
reconsider k = k as Nat by B1;
B3: ( 1 <= k & k <= n + 1 ) by A2, B1, FINSEQ_3:25;

then k <= n by INT_1:7;
then C1: ( k in dom f & k in dom g & k in dom (f (#) g) ) by A0, B3, FINSEQ_3:25;
then ( f . k = fa . k & g . k = gb . k & ((f (#) g) ^ <*(a * b)*>) . k = (f (#) g) . k ) by FINSEQ_1:def 7;
hence (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k by B2, C1, VALUED_1:def 4; :: thesis:

end;

hence (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k by B2; :: thesis:

end;