let x, y be Element of REAL+ ; :: thesis: ( not x *' y = {} or x = {} or y = {} )
assume A1: x *' y = {} ; :: thesis: ( x = {} or y = {} )
assume x <> {} ; :: thesis: y = {}
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
.= (x *' y) *' x1 by ARYTM_2:12
.= {} by A1, ARYTM_2:4 ; :: thesis: verum