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 A2: b in B ; :: thesis: f +* a,b is Function of A,B
X: dom f = A by A2, 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 X, Def3; :: thesis: verum

end;

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

set g = a .--> b;
set f1 = f +* (a .--> b);
A3: a in dom f by A1, A2, FUNCT_2:def 1;
A4: {a} c= A by A1, ZFMISC_1:37;
A5: dom (f +* (a .--> b)) = A \/ (dom (a .--> b)) by X, FUNCT_4:def 1
.= A \/ {a} by FUNCOP_1:19
.= A by A4, XBOOLE_1:12 ;
A6: rng (f +* (a .--> b)) c= (rng f) \/ (rng (a .--> b)) by FUNCT_4:18;
rng (a .--> b) = {b} by FUNCOP_1:14;
then rng (a .--> b) c= B by A2, ZFMISC_1:37;
then (rng f) \/ (rng (a .--> b)) c= B \/ B by XBOOLE_1:13;
then f +* (a .--> b) is Function of A,B by A5, A6, FUNCT_2:4, XBOOLE_1:1;
hence f +* a,b is Function of A,B by A3, Def3; :: thesis: verum

end;

end;