let x be Element of RAT+ ; :: thesis: (numerator x) / (denominator x) = x
A1: denominator x <> {} by Th41;
numerator x, denominator x are_relative_prime by Th40;
then A2: ( RED (numerator x),(denominator x) = numerator x & RED (denominator x),(numerator x) = denominator x ) by Th28;

per cases ( denominator x = 1 or denominator x <> 1 ) ;

suppose A3: denominator x = 1 ; :: thesis: (numerator x) / (denominator x) = x

then x in omega by Th42;
then numerator x = x by Def8;
hence (numerator x) / (denominator x) = x by A2, A3, Def10; :: thesis: verum

end;

suppose A4: denominator x <> 1 ; :: thesis: (numerator x) / (denominator x) = x

then not x in omega by Def9;
then x = [(numerator x),(denominator x)] by Th42;
hence (numerator x) / (denominator x) = x by A1, A2, A4, Def10; :: thesis: verum

end;

end;