let x, y, z be Real; :: thesis: ( 0 <= x implies x * (y -' z) = (x * y) -' (x * z) )
assume A1: x >= 0 ; :: thesis: x * (y -' z) = (x * y) -' (x * z)

per cases ( y - z >= 0 or y - z < 0 ) ;

suppose A2: y - z >= 0 ; :: thesis: x * (y -' z) = (x * y) -' (x * z)

A3: x * (y - z) >= 0 by A1, A2;
thus x * (y -' z) = x * (y - z) by A2, XREAL_0:def 2
.= (x * y) - (x * z)
.= (x * y) -' (x * z) by A3, XREAL_0:def 2 ; :: thesis: verum

end;

suppose A4: y - z < 0 ; :: thesis: x * (y -' z) = (x * y) -' (x * z)

per cases ( x = 0 or x > 0 ) by A1;

suppose A5: x = 0 ; :: thesis: x * (y -' z) = (x * y) -' (x * z)

thus x * (y -' z) = (x * y) -' (x * z) by A5, XREAL_1:232; :: thesis: verum

end;

suppose A6: x > 0 ; :: thesis: x * (y -' z) = (x * y) -' (x * z)

x * (y - z) < 0 by A4, A6;
then A7: (x * y) - (x * z) < 0 ;
thus x * (y -' z) = x * 0 by A4, XREAL_0:def 2
.= (x * y) -' (x * z) by A7, XREAL_0:def 2 ; :: thesis: verum

end;

end;

end;

end;