let a, b be Complex; :: thesis: for n being Nat
for f, g being b₁ -element complex-valued FinSequence holds (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>
let n be Nat; :: thesis: for f, g being n -element complex-valued FinSequence holds (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>
let f, g be n -element complex-valued FinSequence; :: thesis: (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*>
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

proof

let k be object ; :: thesis: ( k in dom (fa (#) gb) implies (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k )
assume B1: k in dom (fa (#) gb) ; :: thesis: (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k
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;

per cases ( k < n + 1 or k = n + 1 ) by B3, XXREAL_0:1;

suppose k < n + 1 ; :: thesis: (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k

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: verum

end;

suppose k = n + 1 ; :: thesis: (fa (#) gb) . k = ((f (#) g) ^ <*(a * b)*>) . k

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

end;

end;

end;

hence (f ^ <*a*>) (#) (g ^ <*b*>) = (f (#) g) ^ <*(a * b)*> by FUNCT_1:2, A3; :: thesis: verum