per cases ( not x in dom f or x in dom f ) ;

suppose not x in dom f ; :: thesis: f +* (x,b) is Function of A,B

hence f +* (x,b) is Function of A,B by FUNCT_7:def 3; :: thesis: verum

end;

suppose x in dom f ; :: thesis: f +* (x,b) is Function of A,B

then A1: B <> {} ;
then dom f = A by FUNCT_2:def 1;
then A2: dom (f +* (x,b)) = A by FUNCT_7:30;
A3: rng f c= B by RELAT_1:def 19;
{b} c= B by A1, ZFMISC_1:31;
then A4: (rng f) \/ {b} c= B by A3, XBOOLE_1:8;
rng (f +* (x,b)) c= (rng f) \/ {b} by FUNCT_7:100;
then rng (f +* (x,b)) c= B by A4;
hence f +* (x,b) is Function of A,B by A2, FUNCT_2:2; :: thesis: verum

end;

end;