let y be set ; :: thesis: 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; :: thesis: for Fy being finite-yielding Function st y in rng Ch holds
Intersection (Fy,Ch,y) is finite
let Fy be finite-yielding Function; :: thesis: ( y in rng Ch implies Intersection (Fy,Ch,y) is finite )
assume y in rng Ch ; :: thesis: Intersection (Fy,Ch,y) is finite
then consider x being set 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 Th33;
hence Intersection (Fy,Ch,y) is finite ; :: thesis: verum