for i, j being Element of omega st i,j are_coprime & j <> {} holds
( numerator (i / j) = i & denominator (i / j) = j )