let A, B, a, b be set ; :: thesis: for f being Function of A,B st a in A & b in B holds
f +* (a .--> b) is Function of A,B
let f be Function of A,B; :: thesis: ( a in A & b in B implies f +* (a .--> b) is Function of A,B )
assume that
A1: a in A and
A2: b in B ; :: thesis: f +* (a .--> b) is Function of A,B
A3: {a} c= A by A1, ZFMISC_1:31;
set g = a .--> b;
set f1 = f +* (a .--> b);
rng (a .--> b) = {b} by FUNCOP_1:8;
then rng (a .--> b) c= B by A2, 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;
dom (f +* (a .--> b)) = (dom f) \/ (dom (a .--> b)) by FUNCT_4:def 1
.= A \/ (dom (a .--> b)) by A2, FUNCT_2:def 1
.= A \/ {a}
.= A by A3, XBOOLE_1:12 ;
hence f +* (a .--> b) is Function of A,B by A4, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum