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