let x1, x2 be set ; :: thesis: for F, Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection F,Ch1,x1 = Intersection F,Ch2,x2
let F be Function; :: thesis: for Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection F,Ch1,x1 = Intersection F,Ch2,x2
let Ch1, Ch2 be Function; :: thesis: ( Ch1 " {x1} = Ch2 " {x2} implies Intersection F,Ch1,x1 = Intersection F,Ch2,x2 )
assume A1: Ch1 " {x1} = Ch2 " {x2} ; :: thesis: Intersection F,Ch1,x1 = Intersection F,Ch2,x2
thus Intersection F,Ch1,x1 c= Intersection F,Ch2,x2 :: according to XBOOLE_0:def 10 :: thesis: Intersection F,Ch2,x2 c= Intersection F,Ch1,x1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch1,x1 or z in Intersection F,Ch2,x2 )
assume A2: z in Intersection F,Ch1,x1 ; :: thesis: z in Intersection F,Ch2,x2

now

let x be set ; :: thesis: ( x in dom Ch2 & Ch2 . x = x2 implies z in F . x )
assume that
A3: x in dom Ch2 and
A4: Ch2 . x = x2 ; :: thesis: z in F . x
Ch2 . x in {x2} by A4, TARSKI:def 1;
then A5: x in Ch1 " {x1} by A1, A3, FUNCT_1:def 13;
then Ch1 . x in {x1} by FUNCT_1:def 13;
then A6: Ch1 . x = x1 by TARSKI:def 1;
x in dom Ch1 by A5, FUNCT_1:def 13;
hence z in F . x by A2, A6, Def2; :: thesis: verum

end;

hence z in Intersection F,Ch2,x2 by A2, Def2; :: thesis: verum

end;

thus Intersection F,Ch2,x2 c= Intersection F,Ch1,x1 :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Intersection F,Ch2,x2 or z in Intersection F,Ch1,x1 )
assume A7: z in Intersection F,Ch2,x2 ; :: thesis: z in Intersection F,Ch1,x1

now

let x be set ; :: thesis: ( x in dom Ch1 & Ch1 . x = x1 implies z in F . x )
assume that
A8: x in dom Ch1 and
A9: Ch1 . x = x1 ; :: thesis: z in F . x
Ch1 . x in {x1} by A9, TARSKI:def 1;
then A10: x in Ch2 " {x2} by A1, A8, FUNCT_1:def 13;
then Ch2 . x in {x2} by FUNCT_1:def 13;
then A11: Ch2 . x = x2 by TARSKI:def 1;
x in dom Ch2 by A10, FUNCT_1:def 13;
hence z in F . x by A7, A11, Def2; :: thesis: verum

end;

hence z in Intersection F,Ch1,x1 by A7, Def2; :: thesis: verum

end;