let x be Element of RAT+ ; :: thesis: x *' one = x
set y = one ;
( (numerator x) *^ 1 = numerator x & (denominator x) *^ 1 = denominator x & numerator one = 1 & denominator one = 1 ) by Def8, Def9, ORDINAL2:56;
hence x *' one = x by Th45; :: thesis: verum