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