let x be set ; :: according to VALUED_2:def 29 :: thesis: ( x in dom (f [+] c) implies (f [+] c) . x is integer-valued Function )
assume x in dom (f [+] c) ; :: thesis: (f [+] c) . x is integer-valued Function
then (f [+] c) . x = c + (f . x) by Def36;
hence (f [+] c) . x is integer-valued Function ; :: thesis: verum