let i be Nat; :: thesis: for c being Complex
for R being i -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let c be Complex; :: thesis: for R being i -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
let R be i -element 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 Th27
.= (Product (i |-> c)) * (Product R) by Th48 ; :: thesis: verum