take
the
PartFunc
of
V
,
A

{}
;
:: thesis:
the
PartFunc
of
V
,
A

{}
is
finite
thus
the
PartFunc
of
V
,
A

{}
is
finite
;
:: thesis:
verum