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