theorem Th50: :: MONOID_0:50

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