the Sorts of A is finite-yielding by MSAFREE2:def 11;
then FreeEnv A is finitely-generated by MSAFREE2:8;
then FreeEnv A is finite-yielding by MSAFREE2:def 13;
then the Sorts of (FreeEnv A) is finite-yielding ;
hence the Sorts of (FreeEnv A) . v is finite ; :: thesis: verum