let x, y, z be Element of RAT+ ; :: thesis: ( x <> {} & x *' y = x *' z implies y = z )
assume x <> {} ; :: thesis: ( not x *' y = x *' z or y = z )
then consider r being Element of RAT+ such that
A1: x *' r = 1 by Th54;
r *' (x *' y) = one *' y by A1, Th52;
then A2: r *' (x *' y) = y by Th53;
r *' (x *' z) = one *' z by A1, Th52;
hence ( not x *' y = x *' z or y = z ) by A2, Th53; :: thesis: verum