for i being natural Number holds Product (i |-> 1) = 1