let S be non empty non void ManySortedSign ; :: thesis: for X being V5() V28() ManySortedSet of holds FreeMSA X is finitely-generated
let X be V5() V28() ManySortedSet of ; :: thesis: FreeMSA X 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 = FreeMSA X holds
ex G being GeneratorSet of A st G is finite-yielding

let S' be non empty non void ManySortedSign ; :: thesis: ( S' = S implies for A being MSAlgebra of S' st A = FreeMSA X holds
ex G being GeneratorSet of A st G is finite-yielding )
assume A1: S' = S ; :: thesis: for A being MSAlgebra of S' st A = FreeMSA X holds
ex G being GeneratorSet of A st G is finite-yielding
let A be MSAlgebra of S'; :: thesis: ( A = FreeMSA X implies ex G being GeneratorSet of A st G is finite-yielding )
assume A2: A = FreeMSA X ; :: thesis: ex G being GeneratorSet of A st G is finite-yielding
reconsider G = FreeGen X as GeneratorSet of FreeMSA X ;
reconsider G = G as GeneratorSet of A by A1, A2;
take G ; :: thesis: G is finite-yielding
thus G is finite-yielding :: thesis: verum

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in the carrier of S' or G . i is finite )
assume i in the carrier of S' ; :: thesis: G . i is finite
then reconsider iS = i as SortSymbol of S by A1;
reconsider Gi = G . i as set ;
reconsider Xi = X . iS as non empty finite set by FINSET_1:def 4;

now

defpred S₁[ set , set ] means $1 = root-tree [$2,i];
A3: for e being set st e in Gi holds
ex u being set st
( u in Xi & S₁[e,u] )

proof

let e be set ; :: thesis: ( e in Gi implies ex u being set st
( u in Xi & S₁[e,u] ) )
assume A4: e in Gi ; :: thesis: ex u being set st
( u in Xi & S₁[e,u] )
Gi = FreeGen iS,X by MSAFREE:def 18;
then consider u being set such that
A5: ( u in Xi & e = root-tree [u,i] ) by A4, MSAFREE:def 17;
take u ; :: thesis: ( u in Xi & S₁[e,u] )
thus ( u in Xi & S₁[e,u] ) by A5; :: thesis: verum

end;

consider f being Function such that
A6: dom f = Gi and
A7: rng f c= Xi and
A8: for e being set st e in Gi holds
S₁[e,f . e] from WELLORD2:sch 1(A3);
take f = f; :: thesis: ex f being Function st
( f is one-to-one & dom f = Gi & rng f c= Xi )
f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume A9: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
hence x1 = root-tree [(f . x2),i] by A6, A8
.= x2 by A6, A8, A9 ;
:: thesis: verum

end;

hence ex f being Function st
( f is one-to-one & dom f = Gi & rng f c= Xi ) by A6, A7; :: thesis: verum

end;

then ( card Gi c= card Xi or card Gi in card Xi ) by CARD_1:26;
hence G . i is finite by CARD_2:68; :: thesis: verum

end;

end;

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

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

end;

end;