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
set g = a .--> b;
set f1 = f +* (a .--> b);
A3: {a} c= A by A1, ZFMISC_1:37;
A4: 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} by FUNCOP_1:19
.= A by A3, XBOOLE_1:12 ;
A5: 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;
hence f +* (a .--> b) is Function of A,B by A4, A5, FUNCT_2:4, XBOOLE_1:1; :: thesis: verum