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 5;
Ch . x in {y} by A2, TARSKI:def 1;
then x in Ch " {y} by A1, FUNCT_1:def 13;
then Intersection Fy,Ch,y c= Fy . x by Th33;
hence Intersection Fy,Ch,y is finite ; :: thesis: verum