set F = f +* (x,n);
let a be object ; :: according to VALUED_0:def 9 :: thesis: ( not a in dom (f +* (x,n)) or not (f +* (x,n)) . a is real )
assume a in dom (f +* (x,n)) ; :: thesis: (f +* (x,n)) . a is real

per cases ( ( x in dom f & x = a ) or ( x in dom f & x <> a ) or not x in dom f ) ;

suppose ( x in dom f & x = a ) ; :: thesis: (f +* (x,n)) . a is real

hence (f +* (x,n)) . a is real by FUNCT_7:31; :: thesis: verum

end;

suppose ( x in dom f & x <> a ) ; :: thesis: (f +* (x,n)) . a is real

then (f +* (x,n)) . a = f . a by FUNCT_7:32;
hence (f +* (x,n)) . a is real ; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: (f +* (x,n)) . a is real

then (f +* (x,n)) . a = f . a by FUNCT_7:def 3;
hence (f +* (x,n)) . a is real ; :: thesis: verum

end;

end;