let r be Real; :: thesis: for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)
let F be real-valued FinSequence; :: thesis: Product (<*r*> ^ F) = r * (Product F)
thus Product (<*r*> ^ F) = (Product <*r*>) * (Product F) by Th97
.= r * (Product F) ; :: thesis: verum