let x, y, z be Element of REAL+ ; :: thesis: ( x <> {} & x *' y = x *' z implies y = z )
assume that
A1: x <> {} and
A2: x *' y = x *' z ; :: thesis: y = z

per cases ( z <=' y or y <=' z ) ;

suppose A3: z <=' y ; :: thesis: y = z

then x *' (y -' z) = (x *' y) - (x *' z) by ARYTM_1:26
.= {} by A2, ARYTM_1:18 ;
then {} = y -' z by A1, ARYTM_1:2
.= y - z by A3, ARYTM_1:def 2 ;
hence y = z by Th6; :: thesis: verum

end;

suppose A4: y <=' z ; :: thesis: y = z

then x *' (z -' y) = (x *' z) - (x *' y) by ARYTM_1:26
.= {} by A2, ARYTM_1:18 ;
then {} = z -' y by A1, ARYTM_1:2
.= z - y by A4, ARYTM_1:def 2 ;
hence y = z by Th6; :: thesis: verum

end;

end;