let y be set ; for Ch being Function
for Fy being finite-yielding Function st y in rng Ch holds
Intersection (Fy,Ch,y) is finite
let Ch be Function; for Fy being finite-yielding Function st y in rng Ch holds
Intersection (Fy,Ch,y) is finite
let Fy be finite-yielding Function; ( y in rng Ch implies Intersection (Fy,Ch,y) is finite )
assume
y in rng Ch
; Intersection (Fy,Ch,y) is finite
then consider x being object such that
A1:
x in dom Ch
and
A2:
Ch . x = y
by FUNCT_1:def 3;
Ch . x in {y}
by A2, TARSKI:def 1;
then
x in Ch " {y}
by A1, FUNCT_1:def 7;
then
Intersection (Fy,Ch,y) c= Fy . x
by Th30;
hence
Intersection (Fy,Ch,y) is finite
; verum