theorem Th7: :: FVALUAT1:7

for x, y, z being ExtReal st ( ( x in REAL & y in REAL ) or z in REAL ) holds
(x + y) / z = (x / z) + (y / z)