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