let c be Complex; :: thesis: for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)
let F be complex-valued FinSequence; :: thesis: Product (<*c*> ^ F) = c * (Product F)
thus Product (<*c*> ^ F) = (Product <*c*>) * (Product F) by RVSUM_1:97
.= c * (Product F) ; :: thesis: verum