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)) and
A2: u in K and
A3: z = (f +* (L --> y)) . u by FUNCT_1:def 12;
A4: dom (L --> y) = L by FUNCOP_1:19;

now

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

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

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

end;

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

then A7: z = f . u by A3, A4, FUNCT_4:12;
u in dom f by A1, A4, A6, FUNCT_4:13;
hence z in f .: K by A2, A7, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

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