let i be natural Number ; :: 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))
reconsider i = i as Nat by TARSKI:1;
reconsider zz = i |-> (z1 * z2) as FinSequence of COMPLEX by Lm5;
Product (i |-> (z1 * z2)) = Product zz
.= multcomplex $$ (i |-> (multcomplex . (z1,z2))) by BINOP_2:def 5
.= multcomplex . ((multcomplex $$ (i |-> z1)),(multcomplex $$ (i |-> z2))) by SETWOP_2:36
.= (Product (i |-> z1)) * (Product (i |-> z2)) by BINOP_2:def 5 ;
hence Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2)) ; :: thesis: verum