let r be real number ; :: 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 Th127
.= r * (Product F) by Th125 ; :: thesis: verum