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;
Product (i |-> ss) = multcomplex $$ (i |-> (multcomplex . (s1,s2))) by BINOP_2:def 5
.= 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