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 Th60;
( r *' (x *' y) = one *' y & r *' (x *' z) = one *' z ) by A1, Th58;
then ( r *' (x *' y) = y & r *' (x *' z) = z ) by Th59;
hence ( not x *' y = x *' z or y = z ) ; :: thesis: verum