let x, y be Element of RAT+ ; :: thesis: ( x <> {} implies ex z being Element of RAT+ st y = x *' z )
reconsider o = one as Element of RAT+ ;
assume x <> {} ; :: thesis: ex z being Element of RAT+ st y = x *' z
then consider z being Element of RAT+ such that
A1: x *' z = 1 by Th54;
take z *' y ; :: thesis: y = x *' (z *' y)
thus y = y *' o by Th53
.= x *' (z *' y) by A1, Th52 ; :: thesis: verum