let i be Nat; :: thesis: for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))
let z1, z2 be Element of COMPLEX ; :: thesis: Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))
thus Product (i |-> (z1 * z2)) = multcomplex $$ (i |-> (multcomplex . z1,z2)) by BINOP_2:def 5
.= multcomplex . (multcomplex $$ (i |-> z1)),(multcomplex $$ (i |-> z2)) by SETWOP_2:47
.= (Product (i |-> z1)) * (Product (i |-> z2)) by BINOP_2:def 5 ; :: thesis: verum