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

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 natural

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

end;

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

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

end;

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

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

end;

end;