let A be non-empty MSAlgebra over S; :: thesis: ( A is finite-yielding implies A is finitely-generated )

assume A1: A is finite-yielding ; :: thesis: A is finitely-generated

assume A1: A is finite-yielding ; :: thesis: A is finitely-generated

per cases
( not S is void or S is void )
;

:: according to MSAFREE2:def 10end;

:: according to MSAFREE2:def 10

case
not S is void
; :: thesis: for S9 being non empty non void ManySortedSign st S9 = S holds

for A being MSAlgebra over S9 st A = A holds

ex G being GeneratorSet of A st G is V39()

for A being MSAlgebra over S9 st A = A holds

ex G being GeneratorSet of A st G is V39()

let S9 be non empty non void ManySortedSign ; :: thesis: ( S9 = S implies for A being MSAlgebra over S9 st A = A holds

ex G being GeneratorSet of A st G is V39() )

assume A2: S9 = S ; :: thesis: for A being MSAlgebra over S9 st A = A holds

ex G being GeneratorSet of A st G is V39()

let A9 be MSAlgebra over S9; :: thesis: ( A9 = A implies ex G being GeneratorSet of A9 st G is V39() )

assume A9 = A ; :: thesis: not for G being GeneratorSet of A9 holds G is V39()

then reconsider G = the Sorts of A as GeneratorSet of A9 by A2, Th6;

take G ; :: thesis: G is V39()

thus G is V39() by A1; :: thesis: verum

end;ex G being GeneratorSet of A st G is V39() )

assume A2: S9 = S ; :: thesis: for A being MSAlgebra over S9 st A = A holds

ex G being GeneratorSet of A st G is V39()

let A9 be MSAlgebra over S9; :: thesis: ( A9 = A implies ex G being GeneratorSet of A9 st G is V39() )

assume A9 = A ; :: thesis: not for G being GeneratorSet of A9 holds G is V39()

then reconsider G = the Sorts of A as GeneratorSet of A9 by A2, Th6;

take G ; :: thesis: G is V39()

thus G is V39() by A1; :: thesis: verum