let x be set ; :: according to VALUED_2:def 28 :: thesis: ( x in dom (</> f) implies (</> f) . x is rational-valued Function )
assume x in dom (</> f) ; :: thesis: (</> f) . x is rational-valued Function
then (</> f) . x = (f . x) " by Def34;
hence (</> f) . x is rational-valued Function ; :: thesis: verum