let x be set ; :: according to VALUED_2:def 27 :: thesis: ( x in dom (f <++> g) implies (f <++> g) . x is real-valued Function )
assume x in dom (f <++> g) ; :: thesis: (f <++> g) . x is real-valued Function
then (f <++> g) . x = (f . x) + (g . x) by Def44;
hence (f <++> g) . x is real-valued Function ; :: thesis: verum