let i be Nat; :: thesis: for c being complex number
for R being i -long FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let c be complex number ; :: thesis: for R being i -long FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let R be i -long FinSequence of COMPLEX ; :: thesis: Product (c * R) = (Product (i |-> c)) * (Product R)
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
thus Product (c * R) = Product (mlt (i |-> s),R) by Th92
.= (Product (i |-> c)) * (Product R) by Th137 ; :: thesis: verum