let A, B, a, b be set ; :: thesis: for f being Function of A,B st b in B holds
f +* (a,b) is Function of A,B
let f be Function of A,B; :: thesis: ( b in B implies f +* (a,b) is Function of A,B )
assume A1: b in B ; :: thesis: f +* (a,b) is Function of A,B
A2: dom f = A by A1, FUNCT_2:def 1;

per cases ( not a in A or a in A ) ;

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

hence f +* (a,b) is Function of A,B by A2, Def2; :: thesis: verum

end;

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

set g = a .--> b;
set f1 = f +* (a .--> b);
rng (a .--> b) = {b} by FUNCOP_1:8;
then rng (a .--> b) c= B by A1, ZFMISC_1:31;
then A4: ( rng (f +* (a .--> b)) c= (rng f) \/ (rng (a .--> b)) & (rng f) \/ (rng (a .--> b)) c= B \/ B ) by FUNCT_4:17, XBOOLE_1:13;
A5: {a} c= A by A3, ZFMISC_1:31;
dom (f +* (a .--> b)) = A \/ (dom (a .--> b)) by A2, FUNCT_4:def 1
.= A \/ {a}
.= A by A5, XBOOLE_1:12 ;
then A6: f +* (a .--> b) is Function of A,B by A4, FUNCT_2:2, XBOOLE_1:1;
a in dom f by A1, A3, FUNCT_2:def 1;
hence f +* (a,b) is Function of A,B by A6, Def2; :: thesis: verum

end;

end;