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 Def46;
hence (f <##> g) . x is rational-valued Function ; :: thesis: verum