let y be set ; for F, Ch being Function st not Intersection (F,Ch,y) is empty holds
Ch " {y} c= dom F
let F, Ch be Function; ( not Intersection (F,Ch,y) is empty implies Ch " {y} c= dom F )
assume
not Intersection (F,Ch,y) is empty
; 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
; 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; verum