let x, y be Element of [.0,1.]; :: thesis: ( x * y = x + y implies x = 0 )

assume x * y = x + y ; :: thesis: x = 0

then z1: y * (1 - x) = - x ;

assume x <> 0 ; :: thesis: contradiction

then ( 0 < x & x <= 1 ) by XXREAL_1:1;

then A4: - x < - 0 by XREAL_1:25;

1 - x in [.0,1.] by OpIn01;

then A2: ( 0 <= 1 - x & 1 - x <= 1 ) by XXREAL_1:1;

y < 0 by A4, A2, z1;

hence contradiction by XXREAL_1:1; :: thesis: verum

assume x * y = x + y ; :: thesis: x = 0

then z1: y * (1 - x) = - x ;

assume x <> 0 ; :: thesis: contradiction

then ( 0 < x & x <= 1 ) by XXREAL_1:1;

then A4: - x < - 0 by XREAL_1:25;

1 - x in [.0,1.] by OpIn01;

then A2: ( 0 <= 1 - x & 1 - x <= 1 ) by XXREAL_1:1;

y < 0 by A4, A2, z1;

hence contradiction by XXREAL_1:1; :: thesis: verum