let r1, r2 be non zero Real; :: thesis: ( |.(x - ((No_omega^ (omega-y x)) * (uReal . r1))).| infinitely< |.x.| & |.(x - ((No_omega^ (omega-y x)) * (uReal . r2))).| infinitely< |.x.| implies r1 = r2 )
assume that
A7: |.(x - ((No_omega^ (omega-y x)) * (uReal . r1))).| infinitely< |.x.| and
A8: |.(x - ((No_omega^ (omega-y x)) * (uReal . r2))).| infinitely< |.x.| ; :: thesis: r1 = r2
|.x.|, No_omega^ (omega-y x) are_commensurate by A1, Def7;
hence r1 = r2 by A7, A8, Lm9; :: thesis: verum