theorem Th107: :: RVSUM_1:107
for i being natural Number
for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)