let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (Re f) or (Re f) . x is real )
assume x in dom (Re f) ; :: thesis: (Re f) . x is real
then (Re f) . x = Re (f . x) by Def3;
hence (Re f) . x is real ; :: thesis: verum