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