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

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,c)) . a is complex

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

end;

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

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

end;

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

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

end;

end;