set F = f +* x,n;
let a be set ; :: according to VALUED_0:def 9 :: thesis: ( not a in dom (f +* x,n) or (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:33; :: 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:34;
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;