let y be set ; :: thesis: for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
Ch " {y} c= dom F
let F, Ch be Function; :: thesis: ( not Intersection (F,Ch,y) is empty implies Ch " {y} c= dom F )
assume not Intersection (F,Ch,y) is empty ; :: thesis: Ch " {y} c= dom F
then consider z being object such that
A1: z in Intersection (F,Ch,y) ;
assume not Ch " {y} c= dom F ; :: thesis: contradiction
then consider x being object such that
A2: x in Ch " {y} and
A3: not x in dom F ;
Ch . x in {y} by A2, FUNCT_1:def 7;
then A4: Ch . x = y by TARSKI:def 1;
x in dom Ch by A2, FUNCT_1:def 7;
then z in F . x by A1, A4, Def2;
hence contradiction by A3, FUNCT_1:def 2; :: thesis: verum