let y, x 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 A3: z in dom F ; :: thesis: y in F . z
( z in dom ((dom F) --> x) & ((dom F) --> x) . z = x ) by A3, FUNCOP_1:13, FUNCOP_1:19;
hence y in F . z by A2, Def2; :: thesis: verum

end;

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