let F be complex-yielding 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;
A1: rng F c= COMPLEX by VALUED_0:def 1;
rng (F ^ <*p*>) c= COMPLEX by VALUED_0:def 1;
then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of COMPLEX by A1, FINSEQ_1:def 4;
thus Product (F ^ <*r*>) = multcomplex $$ Fr by Def14
.= multcomplex . (Product Ff),p by FINSOP_1:5
.= (Product F) * r by BINOP_2:def 5 ; :: thesis: verum