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 object ; :: 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 object 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 6;
A4: dom (L --> y) = L ;

now :: thesis: ( ( u in L & z in {y} ) or ( not u in L & z in f .: K ) )

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:13;
then z = y by A5, FUNCOP_1:7;
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:11;
u in dom f by A1, A4, A6, FUNCT_4:12;
hence z in f .: K by A2, A7, FUNCT_1:def 6; :: thesis: verum

end;

end;

end;

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