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