let F1, F2 be complex-valued FinSequence; :: thesis: Product (F1 ^ F2) = (Product F1) * (Product F2)
A1: rng (F1 ^ F2) c= COMPLEX by VALUED_0:def 1;
( rng F1 c= COMPLEX & rng F2 c= COMPLEX ) by VALUED_0:def 1;
then reconsider FF = F1 ^ F2, f1 = F1, f2 = F2 as FinSequence of COMPLEX by A1, FINSEQ_1:def 4;
thus Product (F1 ^ F2) = multcomplex $$ FF by Def14
.= multcomplex . (Product f1),(Product f2) by FINSOP_1:6
.= (Product F1) * (Product F2) by BINOP_2:def 5 ; :: thesis: verum