let F be complex-valued FinSequence; :: thesis: for r being complex number holds Product (F ^ <*r*>) = (Product F) * r
let r be complex number ; :: thesis: Product (F ^ <*r*>) = (Product F) * r
reconsider p = r as Element of COMPLEX by XCMPLX_0:def 2;
( rng F c= COMPLEX & rng (F ^ <*p*>) c= COMPLEX ) by VALUED_0:def 1;
then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
thus Product (F ^ <*r*>) = multcomplex $$ Fr by Def14
.= multcomplex . ((Product Ff),p) by FINSOP_1:4
.= (Product F) * r by BINOP_2:def 5 ; :: thesis: verum