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