let A, B be non empty set ; :: thesis: for f being Function of A,B
for C being Subset of A
for v being Element of B holds f +* (C --> v) is Function of A,B
let f be Function of A,B; :: thesis: for C being Subset of A
for v being Element of B holds f +* (C --> v) is Function of A,B
let C be Subset of A; :: thesis: for v being Element of B holds f +* (C --> v) is Function of A,B
let v be Element of B; :: thesis: f +* (C --> v) is Function of A,B
A1: dom f = A by FUNCT_2:def 1;
A2: dom (f +* (C --> v)) = (dom f) \/ (dom (C --> v)) by FUNCT_4:def 1
.= ([#] A) \/ C by A1, FUNCOP_1:19
.= A by SUBSET_1:28 ;
A3: rng f c= B by RELSET_1:12;
rng (C --> v) c= {v} by FUNCOP_1:19;
then A4: (rng f) \/ (rng (C --> v)) c= B \/ {v} by A3, XBOOLE_1:13;
rng (f +* (C --> v)) c= (rng f) \/ (rng (C --> v)) by FUNCT_4:18;
then rng (f +* (C --> v)) c= B \/ {v} by A4, XBOOLE_1:1;
then rng (f +* (C --> v)) c= B by ZFMISC_1:46;
hence f +* (C --> v) is Function of A,B by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum