for r1, r2 being Real
for fr1, fr2 being Element of F_Real st r1 = fr1 & r2 = fr2 holds
r1 * r2 = fr1 * fr2 ;