theorem Th39: :: MONOID_0:39

for N being non empty SubStr of <REAL,+>
for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x + y