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

case not S is void ; :: thesis: for b₁ being ManySortedSign holds
( not b₁ = S or for b₂ being MSAlgebra over b₁ holds
( not b₂ = GenMSAlg X or ex b₃ being GeneratorSet of b₂ st b₃ is finite-yielding ) )

let S9 be non empty non void ManySortedSign ; :: thesis: ( not S9 = S or for b₁ being MSAlgebra over S9 holds
( not b₁ = GenMSAlg X or ex b₂ being GeneratorSet of b₁ st b₂ is finite-yielding ) )
assume A1: S9 = S ; :: thesis: for b₁ being MSAlgebra over S9 holds
( not b₁ = GenMSAlg X or ex b₂ being GeneratorSet of b₁ st b₂ is finite-yielding )
let H be MSAlgebra over S9; :: thesis: ( not H = GenMSAlg X or ex b₁ being GeneratorSet of H st b₁ is finite-yielding )
assume A2: H = GenMSAlg X ; :: thesis: ex b₁ being GeneratorSet of H st b₁ is finite-yielding
then reconsider T = X as MSSubset of H by A1, MSUALG_2:def 17;
GenMSAlg T = H by A1, A2, EXTENS_1:18;
then reconsider T = T as GeneratorSet of H by A1, A2, MSAFREE:3;
take T ; :: thesis: T is finite-yielding
thus T is finite-yielding ; :: thesis: verum

end;

case S is void ; :: thesis: the Sorts of (GenMSAlg X) is finite-yielding

hence the Sorts of (GenMSAlg X) is finite-yielding ; :: thesis: verum

end;

end;