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

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

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

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

end;

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

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

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

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

end;

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

x * (y - z) < 0 by S1, S2;
then A1: (x * y) - (x * z) < 0 ;
thus x * (y -' z) = x * 0 by S1, XREAL_0:def 2
.= (x * y) -' (x * z) by A1, XREAL_0:def 2 ; :: thesis: verum

end;

end;

end;

end;