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;
( rng f c= B & rng (C --> v) c= {v} ) by FUNCOP_1:13, RELAT_1:def 19;
then A2: (rng f) \/ (rng (C --> v)) c= B \/ {v} by XBOOLE_1:13;
rng (f +* (C --> v)) c= (rng f) \/ (rng (C --> v)) by FUNCT_4:17;
then rng (f +* (C --> v)) c= B \/ {v} by A2, XBOOLE_1:1;
then A3: rng (f +* (C --> v)) c= B by ZFMISC_1:40;
dom (f +* (C --> v)) = (dom f) \/ (dom (C --> v)) by FUNCT_4:def 1
.= ([#] A) \/ C by A1, FUNCOP_1:13
.= A by SUBSET_1:11 ;
hence f +* (C --> v) is Function of A,B by A3, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum