{} is PartFunc of V,C by RELSET_1:25;
then reconsider e = {} as Element of PFuncs V,C by PARTFUN1:119;
take e ; :: thesis: e is finite
thus e is finite ; :: thesis: verum