the Sorts of A is V33() 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 V33() ;
hence the Sorts of (FreeEnv A) . v is finite ; :: thesis: verum