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