let x, y be Element of RAT+ ; :: thesis: ( x in omega & x + y in omega implies y in omega )
assume that
A1: x in omega and
A2: x + y in omega ; :: thesis: y in omega
A3: denominator (x + y) = 1 by A2, Def9;
set nx = numerator x;
set dx = denominator x;
A4: denominator x = 1 by A1, Def9;
set ny = numerator y;
set dy = denominator y;
A5: ( x + y = (numerator (x + y)) / (denominator (x + y)) & (((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x))) *^ 1 = ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) ) by Th39, ORDINAL2:39;
denominator y <> {} by Th35;
then (denominator x) *^ (denominator y) <> {} by A4, ORDINAL3:31, Lm4;
then ((numerator x) *^ (denominator y)) +^ ((numerator y) *^ (denominator x)) = ((denominator x) *^ (denominator y)) *^ (numerator (x + y)) by A3, A5, Th45, Lm4
.= (denominator y) *^ (numerator (x + y)) by A4, ORDINAL2:39 ;
then ((numerator x) *^ (denominator y)) +^ (numerator y) = (denominator y) *^ (numerator (x + y)) by A4, ORDINAL2:39;
then numerator y = ((denominator y) *^ (numerator (x + y))) -^ ((numerator x) *^ (denominator y)) by ORDINAL3:52;
then numerator y = (denominator y) *^ ((numerator (x + y)) -^ (numerator x)) by ORDINAL3:63;
then A6: denominator y divides numerator y ;
A7: numerator y, denominator y are_coprime by Th34;
for m being natural Ordinal st m divides denominator y & m divides numerator y holds
m divides denominator y ;
then (denominator y) hcf (numerator y) = denominator y by A6, Def5;
then A8: denominator y = 1 by A7, Th20;
y = (numerator y) / (denominator y) by Th39;
then y = numerator y by A8, Th40;
hence y in omega ; :: thesis: verum