let x be object ; :: according to VALUED_0:def 7 :: thesis: ( not x in dom (r + f) or (r + f) . x is complex )
assume x in dom (r + f) ; :: thesis: (r + f) . x is complex
then (r + f) . x = r + (f . x) by Def2;
hence (r + f) . x is complex ; :: thesis: verum