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