let K, L be set ; :: thesis: for x, y being set
for f being Function holds (f +* (L --> y)) .: K c= (f .: K) \/ {y}
let x, y be set ; :: thesis: for f being Function holds (f +* (L --> y)) .: K c= (f .: K) \/ {y}
let f be Function; :: thesis: (f +* (L --> y)) .: K c= (f .: K) \/ {y}
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (f +* (L --> y)) .: K or z in (f .: K) \/ {y} )
assume z in (f +* (L --> y)) .: K ; :: thesis: z in (f .: K) \/ {y}
then consider u being set such that
A1: ( u in dom (f +* (L --> y)) & u in K & z = (f +* (L --> y)) . u ) by FUNCT_1:def 12;
A2: dom (L --> y) = L by FUNCOP_1:19;

now

per cases ( u in L or not u in L ) ;

case A3: u in L ; :: thesis: z in {y}

then z = (L --> y) . u by A1, A2, FUNCT_4:14;
then z = y by A3, FUNCOP_1:13;
hence z in {y} by TARSKI:def 1; :: thesis: verum

end;

case not u in L ; :: thesis: z in f .: K

then ( u in dom f & z = f . u ) by A1, A2, FUNCT_4:12, FUNCT_4:13;
hence z in f .: K by A1, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

hence z in (f .: K) \/ {y} by XBOOLE_0:def 3; :: thesis: verum