let x, y, z be Element of REAL+ ; :: thesis: ( x *' y = x *' z & x <> {} implies y = z )
assume A1: x *' y = x *' z ; :: thesis: ( not x <> {} or y = z )
assume x <> {} ; :: thesis: y = z
then consider x1 being Element of REAL+ such that
A2: x *' x1 = one by ARYTM_2:14;
thus y = (x *' x1) *' y by A2, ARYTM_2:15
.= x1 *' (x *' z) by A1, ARYTM_2:12
.= (x *' x1) *' z by ARYTM_2:12
.= z by A2, ARYTM_2:15 ; :: thesis: verum