let x be set ; :: according to VALUED_0:def 9 :: thesis: ( not x in proj1 (Im f) or (Im f) . x is real )
assume x in dom (Im f) ; :: thesis: (Im f) . x is real
then (Im f) . x = Im (f . x) by Def2a;
hence (Im f) . x is real ; :: thesis: verum