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