let x, y, z be ExtReal; :: thesis: ( ( ( x in REAL & y in REAL ) or z in REAL ) implies (x + y) / z = (x / z) + (y / z) )

assume A1: ( ( x in REAL & y in REAL ) or z in REAL ) ; :: thesis: (x + y) / z = (x / z) + (y / z)

assume A1: ( ( x in REAL & y in REAL ) or z in REAL ) ; :: thesis: (x + y) / z = (x / z) + (y / z)

per cases
( ( x in REAL & y in REAL ) or z in REAL )
by A1;

end;