let c be complex number ; :: 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:127
.= c * (Product F) by RVSUM_1:125 ; :: thesis: verum