take the PartFunc of V,A | {} ; :: thesis: the PartFunc of V,A | {} is finite
thus the PartFunc of V,A | {} is finite ; :: thesis: verum