let x be set ; :: according to VALUED_0:def 10 :: thesis: ( not x in proj1 |.f.| or |.f.| . x is rational )
assume x in dom |.f.| ; :: thesis: |.f.| . x is rational
then |.f.| . x = |.(f . x).| by Def11;
hence |.f.| . x is rational ; :: thesis: verum