let y, X9 be set ; for F, Ch being Function st Ch " {y} = (Ch | X9) " {y} holds
Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)
let F, Ch be Function; ( Ch " {y} = (Ch | X9) " {y} implies Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y) )
assume A1:
Ch " {y} = (Ch | X9) " {y}
; Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)
A2:
Intersection (F,(Ch | X9),y) c= Intersection (F,Ch,y)
proof
let z be
object ;
TARSKI:def 3 ( not z in Intersection (F,(Ch | X9),y) or z in Intersection (F,Ch,y) )
assume A3:
z in Intersection (
F,
(Ch | X9),
y)
;
z in Intersection (F,Ch,y)
hence
z in Intersection (
F,
Ch,
y)
by A3, Def2;
verum
end;
Intersection (F,Ch,y) c= Intersection (F,(Ch | X9),y)
by Th26;
hence
Intersection (F,Ch,y) = Intersection (F,(Ch | X9),y)
by A2; verum