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