let x, y be set ; :: thesis: for F being Function st not F is empty holds
( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds
y in F . z )
let F be Function; :: thesis: ( not F is empty implies ( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds
y in F . z ) )
assume A1: not F is empty ; :: thesis: ( y in Intersection (F,((dom F) --> x),x) iff for z being set st z in dom F holds
y in F . z )
set Ch = (dom F) --> x;
thus ( y in Intersection (F,((dom F) --> x),x) implies for z being set st z in dom F holds
y in F . z ) :: thesis: ( ( for z being set st z in dom F holds
y in F . z ) implies y in Intersection (F,((dom F) --> x),x) )

proof

assume A2: y in Intersection (F,((dom F) --> x),x) ; :: thesis: for z being set st z in dom F holds
y in F . z
let z be set ; :: thesis: ( z in dom F implies y in F . z )
assume z in dom F ; :: thesis: y in F . z
then ( z in dom ((dom F) --> x) & ((dom F) --> x) . z = x ) by FUNCOP_1:7;
hence y in F . z by A2, Def2; :: thesis: verum

end;

((dom F) --> x) " {x} = dom F by FUNCOP_1:15;
then A3: (dom F) /\ (((dom F) --> x) " {x}) = dom F ;
assume for z being set st z in dom F holds
y in F . z ; :: thesis: y in Intersection (F,((dom F) --> x),x)
then for z being set st z in dom ((dom F) --> x) & ((dom F) --> x) . z = x holds
y in F . z ;
hence y in Intersection (F,((dom F) --> x),x) by A1, A3, Th18; :: thesis: verum