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)
per cases ( ( x in REAL & y in REAL ) or z in REAL ) by A1;
suppose ( x in REAL & y in REAL ) ; :: thesis: (x + y) / z = (x / z) + (y / z)
then reconsider x1 = x, y1 = y as Real ;
per cases ( z in REAL or z = +infty or z = -infty ) by XXREAL_0:14;
suppose z in REAL ; :: thesis: (x + y) / z = (x / z) + (y / z)
hence (x + y) / z = (x / z) + (y / z) by XXREAL_3:95; :: thesis: verum
end;
suppose A2: ( z = +infty or z = -infty ) ; :: thesis: (x + y) / z = (x / z) + (y / z)
thus (x + y) / z = 0 + 0 by A2
.= (x / z) + (y / z) by A2 ; :: thesis: verum
end;
end;
end;
suppose z in REAL ; :: thesis: (x + y) / z = (x / z) + (y / z)
hence (x + y) / z = (x / z) + (y / z) by XXREAL_3:95; :: thesis: verum
end;
end;