let i be Nat; :: thesis: for c1, c2 being complex number holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
let c1, c2 be complex number ; :: thesis: Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;
Product (i |-> (s1 * s2)) = multcomplex $$ (i |-> (multcomplex . s1,s2)) by BINOP_2:def 5
.= multcomplex . (multcomplex $$ (i |-> s1)),(multcomplex $$ (i |-> s2)) by SETWOP_2:47
.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def 5 ;
hence Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2)) ; :: thesis: verum