let i be Nat; :: thesis: for c1, c2 being Complex holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))

let c1, c2 be Complex; :: thesis: Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))

reconsider s1 = c1, s2 = c2, ss = c1 * c2 as Element of COMPLEX by XCMPLX_0:def 2;

multcomplex . (c1,c2) = c1 * c2 by BINOP_2:def 5;

then Product (i |-> ss) = multcomplex $$ (i |-> (multcomplex . (s1,s2)))

.= multcomplex . ((multcomplex $$ (i |-> s1)),(multcomplex $$ (i |-> s2))) by SETWOP_2:36

.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def 5 ;

hence Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2)) ; :: thesis: verum

let c1, c2 be Complex; :: thesis: Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))

reconsider s1 = c1, s2 = c2, ss = c1 * c2 as Element of COMPLEX by XCMPLX_0:def 2;

multcomplex . (c1,c2) = c1 * c2 by BINOP_2:def 5;

then Product (i |-> ss) = multcomplex $$ (i |-> (multcomplex . (s1,s2)))

.= multcomplex . ((multcomplex $$ (i |-> s1)),(multcomplex $$ (i |-> s2))) by SETWOP_2:36

.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def 5 ;

hence Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2)) ; :: thesis: verum