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
then A2: x in dom Ch by FUNCT_1:def 13;
Ch . x in {y} by A1, FUNCT_1:def 13;
then A3: Ch . x = y by TARSKI:def 1;
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch,y or z in F . x )
assume z in Intersection F,Ch,y ; :: thesis: z in F . x
hence z in F . x by A2, A3, Def2; :: thesis: verum