let A be non-empty MSAlgebra of S; :: thesis: ( A is locally-finite implies A is finitely-generated )
assume A1: A is locally-finite ; :: thesis: A is finitely-generated

per cases ( not S is void or S is void ) ;
:: according to MSAFREE2:def 10

case not S is void ; :: thesis: for S' being non empty non void ManySortedSign st S' = S holds
for A being MSAlgebra of S' st A = A holds
ex G being GeneratorSet of A st G is locally-finite

let S' be non empty non void ManySortedSign ; :: thesis: ( S' = S implies for A being MSAlgebra of S' st A = A holds
ex G being GeneratorSet of A st G is locally-finite )
assume A2: S' = S ; :: thesis: for A being MSAlgebra of S' st A = A holds
ex G being GeneratorSet of A st G is locally-finite
let A' be MSAlgebra of S'; :: thesis: ( A' = A implies ex G being GeneratorSet of A' st G is locally-finite )
assume A' = A ; :: thesis: ex G being GeneratorSet of A' st G is locally-finite
then reconsider G = the Sorts of A as GeneratorSet of A' by A2, Th9;
take G ; :: thesis: G is locally-finite
thus G is locally-finite by A1, Def11; :: thesis: verum

end;

case S is void ; :: thesis: the Sorts of A is locally-finite

thus the Sorts of A is locally-finite by A1, Def11; :: thesis: verum

end;

end;