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

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