let F be Function; :: thesis: for x1, x2 being object
for Ch1, Ch2 being Function st Ch1 " {x1} = Ch2 " {x2} holds
Intersection (F,Ch1,x1) = Intersection (F,Ch2,x2)
let x1, x2 be object ; :: 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 object ; :: 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 :: thesis: for x being set st x in dom Ch2 & Ch2 . x = x2 holds
z in F . x
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 7;
then Ch1 . x in {x1} by FUNCT_1:def 7;
then A6: Ch1 . x = x1 by TARSKI:def 1;
x in dom Ch1 by A5, FUNCT_1:def 7;
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 object ; :: 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 :: thesis: for x being set st x in dom Ch1 & Ch1 . x = x1 holds
z in F . x
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 7;
then Ch2 . x in {x2} by FUNCT_1:def 7;
then A11: Ch2 . x = x2 by TARSKI:def 1;
x in dom Ch2 by A10, FUNCT_1:def 7;
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;