theorem :: RELSET_3:23

for r1, r2 being Real holds (addRel (REAL,r1)) * (addRel (REAL,r2)) = addRel (REAL,(r1 + r2))