let x be object ; :: according to VALUED_0:def 9 :: thesis: ( not x in dom (f1 + f2) or not (f1 + f2) . x is real )
assume x in dom (f1 + f2) ; :: thesis: (f1 + f2) . x is real
then (f1 + f2) . x = (f1 . x) + (f2 . x) by Def1;
hence (f1 + f2) . x is real ; :: thesis: verum