let i, j be Nat; :: thesis: for c being Complex holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
let c be Complex; :: thesis: Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
Product ((i + j) |-> s) = multcomplex . ((multcomplex $$ (i |-> s)),(multcomplex $$ (j |-> s))) by SETWOP_2:26
.= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def 5 ;
hence Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c)) ; :: thesis: verum