let x, y be set ; :: thesis: for Ch, F being Function st x in Ch " {y} holds
Intersection F,Ch,y c= F . x
let Ch, F be Function; :: thesis: ( x in Ch " {y} implies Intersection F,Ch,y c= F . x )
assume A1: x in Ch " {y} ; :: thesis: Intersection F,Ch,y c= F . x
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch,y or z in F . x )
assume A2: z in Intersection F,Ch,y ; :: thesis: z in F . x
Ch . x in {y} by A1, FUNCT_1:def 13;
then ( x in dom Ch & Ch . x = y ) by A1, FUNCT_1:def 13, TARSKI:def 1;
hence z in F . x by A2, Def2; :: thesis: verum