let F be Function; :: thesis: for i, xi being set
for Ai being Subset of (F . i) st (proj F,i) " {xi} meets (proj F,i) " Ai holds
xi in Ai
let i, xi be set ; :: thesis: for Ai being Subset of (F . i) st (proj F,i) " {xi} meets (proj F,i) " Ai holds
xi in Ai
let Ai be Subset of (F . i); :: thesis: ( (proj F,i) " {xi} meets (proj F,i) " Ai implies xi in Ai )
consider f being Element of ((proj F,i) " {xi}) /\ ((proj F,i) " Ai);
assume A1: ((proj F,i) " {xi}) /\ ((proj F,i) " Ai) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: xi in Ai
then f in (proj F,i) " {xi} by XBOOLE_0:def 4;
then (proj F,i) . f in {xi} by FUNCT_1:def 13;
then A2: (proj F,i) . f = xi by TARSKI:def 1;
f in (proj F,i) " Ai by A1, XBOOLE_0:def 4;
hence xi in Ai by A2, FUNCT_1:def 13; :: thesis: verum