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 Def13
.= multcomplex . ((Product f1),(Product f2)) by FINSOP_1:5
.= (Product F1) * (Product F2) by BINOP_2:def 5 ; :: thesis: verum