for R being Element of 0 -tuples_on COMPLEX holds Product R = 1 by Lm3;