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