let x be Element of RAT+ ; :: thesis: x *' {} = {}
( denominator {} = 1 & numerator {} = {} & (numerator x) *^ {} = {} & (denominator x) *^ 1 = denominator x ) by Def8, Def9, Lm1, ORDINAL2:52, ORDINAL2:56;
hence x *' {} = {} by Th46; :: thesis: verum