{} 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