let S be non empty non void ManySortedSign ; :: thesis: for X being V5() V39() ManySortedSet of the carrier of S holds FreeMSA X is finitely-generated

let X be V5() V39() ManySortedSet of the carrier of S; :: thesis: FreeMSA X is finitely-generated

let X be V5() V39() ManySortedSet of the carrier of S; :: thesis: FreeMSA X 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 = FreeMSA X holds

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

for A being MSAlgebra over S9 st A = FreeMSA X holds

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

reconsider G = FreeGen X as GeneratorSet of FreeMSA X ;

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

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

assume A1: S9 = S ; :: thesis: for A being MSAlgebra over S9 st A = FreeMSA X holds

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

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

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

then reconsider G = G as GeneratorSet of A by A1;

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

thus G is V39() :: thesis: verum

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

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

assume A1: S9 = S ; :: thesis: for A being MSAlgebra over S9 st A = FreeMSA X holds

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

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

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

then reconsider G = G as GeneratorSet of A by A1;

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

thus G is V39() :: thesis: verum

proof

let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in the carrier of S9 or G . i is finite )

reconsider Gi = G . i as set ;

assume i in the carrier of S9 ; :: thesis: G . i is finite

then reconsider iS = i as SortSymbol of S by A1;

reconsider Xi = X . iS as non empty finite set ;

hence G . i is finite by CARD_2:49; :: thesis: verum

end;reconsider Gi = G . i as set ;

assume i in the carrier of S9 ; :: thesis: G . i is finite

then reconsider iS = i as SortSymbol of S by A1;

reconsider Xi = X . iS as non empty finite set ;

now :: thesis: ex f, f being Function st

( f is one-to-one & dom f = Gi & rng f c= Xi )

then
( card Gi c= card Xi or card Gi in card Xi )
by CARD_1:10;( f is one-to-one & dom f = Gi & rng f c= Xi )

defpred S_{1}[ object , object ] means $1 = root-tree [$2,i];

A2: for e being object st e in Gi holds

ex u being object st

( u in Xi & S_{1}[e,u] )

A5: dom f = Gi and

A6: rng f c= Xi and

A7: for e being object st e in Gi holds

S_{1}[e,f . e]
from FUNCT_1:sch 6(A2);

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

( f is one-to-one & dom f = Gi & rng f c= Xi ) by A5, A6; :: thesis: verum

end;A2: for e being object st e in Gi holds

ex u being object st

( u in Xi & S

proof

consider f being Function such that
A3:
Gi = FreeGen (iS,X)
by MSAFREE:def 16;

let e be object ; :: thesis: ( e in Gi implies ex u being object st

( u in Xi & S_{1}[e,u] ) )

assume e in Gi ; :: thesis: ex u being object st

( u in Xi & S_{1}[e,u] )

then consider u being set such that

A4: ( u in Xi & e = root-tree [u,i] ) by A3, MSAFREE:def 15;

take u ; :: thesis: ( u in Xi & S_{1}[e,u] )

thus ( u in Xi & S_{1}[e,u] )
by A4; :: thesis: verum

end;let e be object ; :: thesis: ( e in Gi implies ex u being object st

( u in Xi & S

assume e in Gi ; :: thesis: ex u being object st

( u in Xi & S

then consider u being set such that

A4: ( u in Xi & e = root-tree [u,i] ) by A3, MSAFREE:def 15;

take u ; :: thesis: ( u in Xi & S

thus ( u in Xi & S

A5: dom f = Gi and

A6: rng f c= Xi and

A7: for e being object st e in Gi holds

S

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

hence
ex f being Function st
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A8: x1 in dom f and

A9: x2 in dom f and

A10: f . x1 = f . x2 ; :: thesis: x1 = x2

thus x1 = root-tree [(f . x2),i] by A5, A7, A8, A10

.= x2 by A5, A7, A9 ; :: thesis: verum

end;assume that

A8: x1 in dom f and

A9: x2 in dom f and

A10: f . x1 = f . x2 ; :: thesis: x1 = x2

thus x1 = root-tree [(f . x2),i] by A5, A7, A8, A10

.= x2 by A5, A7, A9 ; :: thesis: verum

( f is one-to-one & dom f = Gi & rng f c= Xi ) by A5, A6; :: thesis: verum

hence G . i is finite by CARD_2:49; :: thesis: verum