:: MSAFREE semantic presentation

begin

theorem Th1: :: MSAFREE:1
for I being set
for J being non empty set
for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
proof
let I be set ; ::_thesis: for J being non empty set
for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
let J be non empty set ; ::_thesis: for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
let f be Function of I,(J *); ::_thesis: for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
let X be ManySortedSet of J; ::_thesis: for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
let p be Element of J * ; ::_thesis: for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)
let x be set ; ::_thesis: ( x in I & p = f . x implies ((X #) * f) . x = product (X * p) )
assume A1: ( x in I & p = f . x ) ; ::_thesis: ((X #) * f) . x = product (X * p)
A2: dom f = I by FUNCT_2:def_1;
then  dom ((X #) * f) = dom f by PARTFUN1:def_2;
hence ((X #) * f) . x = (X #) . p by A1, A2, FUNCT_1:12
.= product (X * p) by FINSEQ_2:def_5 ;
::_thesis: verum
end;

definition
let I be set ;
let A, B be ManySortedSet of I;
let C be ManySortedSubset of A;
let F be ManySortedFunction of A,B;
funcF || C ->  ManySortedFunction of C,B means :Def1: :: MSAFREE:def 1
 for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
it . i = f | (C . i);
existence
 ex b1 being ManySortedFunction of C,B st
for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i)
proof
defpred S1[ set , set ] means  for f being Function of (A . $1),(B . $1) st f = F . $1 holds
$2 = f | (C . $1);
A1: for i being set st i in I holds
ex u being set st S1[i,u]
proof
let i be set ; ::_thesis: ( i in I implies ex u being set st S1[i,u] )
assume  i in I ; ::_thesis: ex u being set st S1[i,u]
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
take  f | (C . i) ; ::_thesis: S1[i,f | (C . i)]
thus  S1[i,f | (C . i)] ; ::_thesis: verum
end;
consider H being Function such that
A2: ( dom H = I & ( for i being set st i in I holds
S1[i,H . i] ) ) from CLASSES1:sch_1(A1);
reconsider H = H as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for i being set st i in I holds
H . i is Function of (C . i),(B . i)
proof
let i be set ; ::_thesis: ( i in I implies H . i is Function of (C . i),(B . i) )
assume A3: i in I ; ::_thesis: H . i is Function of (C . i),(B . i)
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
A4: H . i = f | (C . i) by A2, A3;
 C c= A by PBOOLE:def_18;
then A5: C . i c= A . i by A3, PBOOLE:def_2;
percases ( B . i is empty or not B . i is empty ) ;
supposeA6: B . i is empty ; ::_thesis: H . i is Function of (C . i),(B . i)
then A7: H . i = {} by A4;
now__::_thesis:_H_._i_is_Function_of_(C_._i),(B_._i)
percases ( C . i = {} or C . i <> {} ) ;
suppose C . i = {} ; ::_thesis: H . i is Function of (C . i),(B . i)
hence  H . i is Function of (C . i),(B . i) by A7, RELSET_1:12; ::_thesis: verum
end;
suppose C . i <> {} ; ::_thesis: H . i is Function of (C . i),(B . i)
thus  H . i is Function of (C . i),(B . i) by A6, A7, FUNCT_2:def_1, RELSET_1:12; ::_thesis: verum
end;
end;
end;
hence  H . i is Function of (C . i),(B . i) ; ::_thesis: verum
end;
supposeA8: not B . i is empty ; ::_thesis: H . i is Function of (C . i),(B . i)
then A9: dom f = A . i by FUNCT_2:def_1;
A10: rng (f | (C . i)) c= B . i by RELAT_1:def_19;
dom (f | (C . i)) = (dom f) /\ (C . i) by RELAT_1:61
.= C . i by A5, A9, XBOOLE_1:28 ;
hence  H . i is Function of (C . i),(B . i) by A4, A8, A10, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
end;
then reconsider H = H as ManySortedFunction of C,B by PBOOLE:def_15;
take  H ; ::_thesis: for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
H . i = f | (C . i)
thus  for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
H . i = f | (C . i) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of C,B st ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b1 . i = f | (C . i) ) & ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b2 . i = f | (C . i) ) holds
b1 = b2
proof
let X, Y be ManySortedFunction of C,B; ::_thesis: ( ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
X . i = f | (C . i) ) & ( for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
Y . i = f | (C . i) ) implies X = Y )
assume that
A11: for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
X . i = f | (C . i) and
A12: for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
Y . i = f | (C . i) ; ::_thesis: X = Y
 for i being set st i in I holds
X . i = Y . i
proof
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A13: i in I ; ::_thesis: X . i = Y . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
 X . i = f | (C . i) by A11, A13;
hence  X . i = Y . i by A12, A13; ::_thesis: verum
end;
hence  X = Y by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines || MSAFREE:def_1_:_
 for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for b6 being ManySortedFunction of C,B holds
( b6 = F || C iff for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
b6 . i = f | (C . i) );

definition
let I be set ;
let X be ManySortedSet of I;
let i be set ;
assume A1: i in I ;
func coprod (i,X) ->  set  means :Def2: :: MSAFREE:def 2
 for x being set holds
( x in it iff ex a being set st
( a in X . i & x = [a,i] ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) )
proof
defpred S1[ set ] means  ex a being set st
( a in X . i & $1 = [a,i] );
consider A being set  such that
A2: for x being set holds
( x in A iff ( x in [:(X . i),I:] & S1[x] ) ) from XBOOLE_0:sch_1();
take  A ; ::_thesis: for x being set holds
( x in A iff ex a being set st
( a in X . i & x = [a,i] ) )
let x be set ; ::_thesis: ( x in A iff ex a being set st
( a in X . i & x = [a,i] ) )
thus  ( x in A implies ex a being set st
( a in X . i & x = [a,i] ) ) by A2; ::_thesis: ( ex a being set st
( a in X . i & x = [a,i] ) implies x in A )
given a being set  such that A3: ( a in X . i & x = [a,i] ) ; ::_thesis: x in A
 x in [:(X . i),I:] by A1, A3, ZFMISC_1:87;
hence  x in A by A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . i & x = [a,i] ) ) ) holds
b1 = b2
proof
let A, B be set ; ::_thesis: ( ( for x being set holds
( x in A iff ex a being set st
( a in X . i & x = [a,i] ) ) ) & ( for x being set holds
( x in B iff ex a being set st
( a in X . i & x = [a,i] ) ) ) implies A = B )
assume that
A4: for x being set holds
( x in A iff ex a being set st
( a in X . i & x = [a,i] ) ) and
A5: for x being set holds
( x in B iff ex a being set st
( a in X . i & x = [a,i] ) ) ; ::_thesis: A = B
thus  A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
then  ex a being set st
( a in X . i & x = [a,i] ) by A4;
hence  x in B by A5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume  x in B ; ::_thesis: x in A
then  ex a being set st
( a in X . i & x = [a,i] ) by A5;
hence  x in A by A4; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines coprod MSAFREE:def_2_:_
 for I being set
for X being ManySortedSet of I
for i being set st i in I holds
for b4 being set holds
( b4 = coprod (i,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . i & x = [a,i] ) ) );

notation
let I be set ;
let X be ManySortedSet of I;
synonym  coprod X for  disjoin I;
end;

registration
let I be set ;
let X be ManySortedSet of I;
cluster coprod  -> I -defined ;
coherence
 coprod is I -defined
proof
 dom (coprod ) = dom X by CARD_3:def_3;
then  dom (coprod ) = I by PARTFUN1:def_2;
hence  coprod is I -defined by RELAT_1:def_18; ::_thesis: verum
end;
end;

registration
let I be set ;
let X be ManySortedSet of I;
cluster coprod  ->  total ;
coherence
 coprod is total
proof
 dom (coprod ) = dom X by CARD_3:def_3;
then  dom (coprod ) = I by PARTFUN1:def_2;
hence  coprod is total by PARTFUN1:def_2; ::_thesis: verum
end;
end;

definition
let I be set ;
let X be ManySortedSet of I;
:: original: coprod
redefine func coprod X ->  set  means :Def3: :: MSAFREE:def 3
( dom it = I & ( for i being set st i in I holds
it . i = coprod (i,X) ) );
compatibility
 for b1 being set holds
( b1 = coprod iff ( dom b1 = I & ( for i being set st i in I holds
b1 . i = coprod (i,X) ) ) )
proof
let IT be Function; ::_thesis: ( IT = coprod iff ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) ) )
hereby  ::_thesis: ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) implies IT = coprod )
assume A1: IT = disjoin X ; ::_thesis: ( dom IT = I & ( for i being set st i in I holds
IT . i = coprod (i,X) ) )
hence  dom IT = I by PARTFUN1:def_2; ::_thesis: for i being set st i in I holds
IT . i = coprod (i,X)
let i be set ; ::_thesis: ( i in I implies IT . i = coprod (i,X) )
assume A2: i in I ; ::_thesis: IT . i = coprod (i,X)
then  i in dom X by PARTFUN1:def_2;
then A3: IT . i = [:(X . i),{i}:] by A1, CARD_3:def_3;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_IT_._i_implies_ex_a_being_set_st_
(_a_in_X_._i_&_x_=_[a,i]_)_)_&_(_ex_a_being_set_st_
(_a_in_X_._i_&_x_=_[a,i]_)_implies_x_in_IT_._i_)_)
let x be set ; ::_thesis: ( ( x in IT . i implies ex a being set st
( a in X . i & x = [a,i] ) ) & ( ex a being set st
( a in X . i & x = [a,i] ) implies x in IT . i ) )
hereby  ::_thesis: ( ex a being set st
( a in X . i & x = [a,i] ) implies x in IT . i )
assume  x in IT . i ; ::_thesis: ex a being set st
( a in X . i & x = [a,i] )
then consider a, b being set  such that
A4: a in X . i and
A5: ( b in {i} & x = [a,b] ) by A3, ZFMISC_1:def_2;
take a = a; ::_thesis: ( a in X . i & x = [a,i] )
thus  a in X . i by A4; ::_thesis: x = [a,i]
thus  x = [a,i] by A5, TARSKI:def_1; ::_thesis: verum
end;
given a being set  such that A6: ( a in X . i & x = [a,i] ) ; ::_thesis: x in IT . i
 i in {i} by TARSKI:def_1;
hence  x in IT . i by A3, A6, ZFMISC_1:def_2; ::_thesis: verum
end;
hence  IT . i = coprod (i,X) by A2, Def2; ::_thesis: verum
end;
assume that
A7: dom IT = I and
A8: for i being set st i in I holds
IT . i = coprod (i,X) ; ::_thesis: IT = coprod
A9: dom IT = dom X by A7, PARTFUN1:def_2;
now__::_thesis:_for_x_being_set_st_x_in_dom_X_holds_
IT_._x_=_[:(X_._x),{x}:]
let x be set ; ::_thesis: ( x in dom X implies IT . x = [:(X . x),{x}:] )
assume A10: x in dom X ; ::_thesis: IT . x = [:(X . x),{x}:]
then A11: x in I ;
A12: now__::_thesis:_for_a_being_set_holds_
(_(_a_in_coprod_(x,X)_implies_a_in_[:(X_._x),{x}:]_)_&_(_a_in_[:(X_._x),{x}:]_implies_a_in_coprod_(x,X)_)_)
let a be set ; ::_thesis: ( ( a in coprod (x,X) implies a in [:(X . x),{x}:] ) & ( a in [:(X . x),{x}:] implies a in coprod (x,X) ) )
hereby  ::_thesis: ( a in [:(X . x),{x}:] implies a in coprod (x,X) )
assume  a in coprod (x,X) ; ::_thesis: a in [:(X . x),{x}:]
then A13: ex b being set st
( b in X . x & a = [b,x] ) by A11, Def2;
 x in {x} by TARSKI:def_1;
hence  a in [:(X . x),{x}:] by A13, ZFMISC_1:def_2; ::_thesis: verum
end;
assume  a in [:(X . x),{x}:] ; ::_thesis: a in coprod (x,X)
then consider a1, a2 being set  such that
A14: a1 in X . x and
A15: a2 in {x} and
A16: a = [a1,a2] by ZFMISC_1:def_2;
 a2 = x by A15, TARSKI:def_1;
hence  a in coprod (x,X) by A11, A14, A16, Def2; ::_thesis: verum
end;
thus IT . x = coprod (x,X) by A8, A10
.= [:(X . x),{x}:] by A12, TARSKI:1 ; ::_thesis: verum
end;
hence  IT = coprod by A9, CARD_3:def_3; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines coprod MSAFREE:def_3_:_
 for I being set
for X being ManySortedSet of I
for b3 being set holds
( b3 = coprod X iff ( dom b3 = I & ( for i being set st i in I holds
b3 . i = coprod (i,X) ) ) );

registration
let I be non empty set ;
let X be V16() ManySortedSet of I;
cluster coprod  -> V16() ;
coherence
 coprod X is non-empty
proof
now__::_thesis:_for_x_being_set_st_x_in_I_holds_
not_(coprod_X)_._x_is_empty
let x be set ; ::_thesis: ( x in I implies not (coprod X) . x is empty )
assume  x in I ; ::_thesis: not (coprod X) . x is empty
then reconsider i = x as Element of I ;
consider a being set  such that
A1: a in X . i by XBOOLE_0:def_1;
 (coprod X) . i = coprod (i,X) by Def3;
then  [a,i] in (coprod X) . i by A1, Def2;
hence  not (coprod X) . x is empty ; ::_thesis: verum
end;
hence  coprod X is non-empty by PBOOLE:def_13; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let X be V16() ManySortedSet of I;
cluster Union X ->  non empty ;
coherence
 not Union X is empty
proof
set i = the Element of I;
consider a being set  such that
A1: a in X . the Element of I by XBOOLE_0:def_1;
 dom X = I by PARTFUN1:def_2;
then  X . the Element of I in rng X by FUNCT_1:def_3;
then  a in union (rng X) by A1, TARSKI:def_4;
hence  not Union X is empty by CARD_3:def_4; ::_thesis: verum
end;
end;

theorem :: MSAFREE:2
for I being set
for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
proof
let I be set ; ::_thesis: for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
let X be ManySortedSet of I; ::_thesis: for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )
let i be set ; ::_thesis: ( i in I implies ( X . i <> {} iff (coprod X) . i <> {} ) )
assume A1: i in I ; ::_thesis: ( X . i <> {} iff (coprod X) . i <> {} )
then A2: (coprod X) . i = coprod (i,X) by Def3;
thus  ( X . i <> {} implies (coprod X) . i <> {} ) ::_thesis: ( (coprod X) . i <> {} implies X . i <> {} )
proof
assume  X . i <> {} ; ::_thesis: (coprod X) . i <> {}
then consider x being set  such that
A3: x in X . i by XBOOLE_0:def_1;
 [x,i] in (coprod X) . i by A1, A2, A3, Def2;
hence  (coprod X) . i <> {} ; ::_thesis: verum
end;
assume  (coprod X) . i <> {} ; ::_thesis: X . i <> {}
then consider a being set  such that
A4: a in coprod (i,X) by A2, XBOOLE_0:def_1;
 ex x being set st
( x in X . i & a = [x,i] ) by A1, A4, Def2;
hence  X . i <> {} ; ::_thesis: verum
end;

begin


definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
mode GeneratorSet of U0 ->  MSSubset of U0 means :Def4: :: MSAFREE:def 4
 the Sorts of (GenMSAlg it) = the Sorts of U0;
existence
 ex b1 being MSSubset of U0 st the Sorts of (GenMSAlg b1) = the Sorts of U0
proof
set A = the Sorts of U0;
reconsider A = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
take  A ; ::_thesis: the Sorts of (GenMSAlg A) = the Sorts of U0
set G = GenMSAlg A;
 the Sorts of (GenMSAlg A) is MSSubset of U0 by MSUALG_2:def_9;
then A1: the Sorts of (GenMSAlg A) c= A by PBOOLE:def_18;
 A is MSSubset of (GenMSAlg A) by MSUALG_2:def_17;
then  A c= the Sorts of (GenMSAlg A) by PBOOLE:def_18;
hence  the Sorts of (GenMSAlg A) = the Sorts of U0 by A1, PBOOLE:146; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def_4_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b3 being MSSubset of U0 holds
( b3 is GeneratorSet of U0 iff the Sorts of (GenMSAlg b3) = the Sorts of U0 );

theorem :: MSAFREE:3
for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra over S
for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U0 being strict non-empty MSAlgebra over S
for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
let U0 be strict non-empty MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
let A be MSSubset of U0; ::_thesis: ( A is GeneratorSet of U0 iff GenMSAlg A = U0 )
thus  ( A is GeneratorSet of U0 implies GenMSAlg A = U0 ) ::_thesis: ( GenMSAlg A = U0 implies A is GeneratorSet of U0 )
proof
reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
assume  A is GeneratorSet of U0 ; ::_thesis: GenMSAlg A = U0
then  the Sorts of (GenMSAlg A) = the Sorts of U1 by Def4;
hence  GenMSAlg A = U0 by MSUALG_2:9; ::_thesis: verum
end;
assume  GenMSAlg A = U0 ; ::_thesis: A is GeneratorSet of U0
hence  A is GeneratorSet of U0 by Def4; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let IT be GeneratorSet of U0;
attrIT is free  means :Def5: :: MSAFREE:def 5
 for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h || IT = f );
end;

:: deftheorem Def5 defines free MSAFREE:def_5_:_
 for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for IT being GeneratorSet of U0 holds
( IT is free iff for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h || IT = f ) );

definition
let S be non empty non void ManySortedSign ;
let IT be MSAlgebra over S;
attrIT is free  means :Def6: :: MSAFREE:def 6
 ex G being GeneratorSet of IT st G is free ;
end;

:: deftheorem Def6 defines free MSAFREE:def_6_:_
 for S being non empty non void ManySortedSign
for IT being MSAlgebra over S holds
( IT is free iff ex G being GeneratorSet of IT st G is free );

theorem Th4: :: MSAFREE:4
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
let X be ManySortedSet of the carrier of S; ::_thesis: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]
assume  (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being set  such that
A1: x in (Union (coprod X)) /\ [: the carrier' of S,{ the carrier of S}:] by XBOOLE_0:def_1;
 x in Union (coprod X) by A1, XBOOLE_0:def_4;
then  x in union (rng (coprod X)) by CARD_3:def_4;
then consider A being set  such that
A2: x in A and
A3: A in rng (coprod X) by TARSKI:def_4;
consider s being set  such that
A4: s in dom (coprod X) and
A5: (coprod X) . s = A by A3, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A4;
 A = coprod (s,X) by A5, Def3;
then A6: ex a being set st
( a in X . s & x = [a,s] ) by A2, Def2;
 x in [: the carrier' of S,{ the carrier of S}:] by A1, XBOOLE_0:def_4;
then  s in { the carrier of S} by A6, ZFMISC_1:87;
then  ( s in the carrier of S & s = the carrier of S ) by TARSKI:def_1;
hence  contradiction ; ::_thesis: verum
end;

begin

definition
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
func REL X ->  Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) means :Def7: :: MSAFREE:def 7
 for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) );
existence
 ex b1 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
proof
set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
defpred S1[ Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)), Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ] means ( $1 in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = $1 holds
( len $2 = len (the_arity_of o) & ( for x being set st x in dom $2 holds
( ( $2 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = $2 . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( $2 . x in Union (coprod X) implies $2 . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) );
consider R being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) such that
A1: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff S1[a,b] ) from RELSET_1:sch_2();
take  R ; ::_thesis: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
let a be Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)); ::_thesis: for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
let b be Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ; ::_thesis: ( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) )
thus  ( [a,b] in R implies ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) by A1; ::_thesis: ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) implies [a,b] in R )
assume  ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ; ::_thesis: [a,b] in R
hence  [a,b] in R by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b2 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) holds
b1 = b2
proof
set O = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
let R, P be Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *); ::_thesis: ( ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in P iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ) implies R = P )
assume that
A2: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in R iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) and
A3: for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in P iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) ; ::_thesis: R = P
 for x, y being set holds
( [x,y] in R iff [x,y] in P )
proof
let x, y be set ; ::_thesis: ( [x,y] in R iff [x,y] in P )
thus  ( [x,y] in R implies [x,y] in P ) ::_thesis: ( [x,y] in P implies [x,y] in R )
proof
assume A4: [x,y] in R ; ::_thesis: [x,y] in P
then reconsider a = x as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87;
reconsider b = y as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A4, ZFMISC_1:87;
 [a,b] in R by A4;
then A5: a in [: the carrier' of S,{ the carrier of S}:] by A2;
 for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) by A2, A4;
hence  [x,y] in P by A3, A5; ::_thesis: verum
end;
assume A6: [x,y] in P ; ::_thesis: [x,y] in R
then reconsider a = x as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:87;
reconsider b = y as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A6, ZFMISC_1:87;
 [a,b] in P by A6;
then A7: a in [: the carrier' of S,{ the carrier of S}:] by A3;
 for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) by A3, A6;
hence  [x,y] in R by A2, A7; ::_thesis: verum
end;
hence  R = P by RELAT_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines REL MSAFREE:def_7_:_
 for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for b3 being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) holds
( b3 = REL X iff for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b3 iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) ) );


theorem Th5: :: MSAFREE:5
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
let o be OperSymbol of S; ::_thesis: for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
let b be Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ; ::_thesis: ( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )
defpred S1[ OperSymbol of S, Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * ] means ( len $2 = len (the_arity_of $1) & ( for x being set st x in dom $2 holds
( ( $2 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = $2 . x holds
the_result_sort_of o1 = (the_arity_of $1) . x ) & ( $2 . x in Union (coprod X) implies b . x in coprod (((the_arity_of $1) . x),X) ) ) ) );
set a = [o, the carrier of S];
 the carrier of S in { the carrier of S} by TARSKI:def_1;
then A1: [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then reconsider a = [o, the carrier of S] as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def_3;
thus  ( [[o, the carrier of S],b] in REL X implies S1[o,b] ) ::_thesis: ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) implies [[o, the carrier of S],b] in REL X )
proof
assume  [[o, the carrier of S],b] in REL X ; ::_thesis: S1[o,b]
then  for o1 being OperSymbol of S st [o1, the carrier of S] = a holds
S1[o1,b] by Def7;
hence  S1[o,b] ; ::_thesis: verum
end;
assume A2: S1[o,b] ; ::_thesis: [[o, the carrier of S],b] in REL X
now__::_thesis:_for_o1_being_OperSymbol_of_S_st_[o1,_the_carrier_of_S]_=_a_holds_
S1[o1,b]
let o1 be OperSymbol of S; ::_thesis: ( [o1, the carrier of S] = a implies S1[o1,b] )
assume  [o1, the carrier of S] = a ; ::_thesis: S1[o1,b]
then  o1 = o by XTUPLE_0:1;
hence  S1[o1,b] by A2; ::_thesis: verum
end;
hence  [[o, the carrier of S],b] in REL X by A1, Def7; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
func DTConMSA X ->  DTConstrStr  equals :: MSAFREE:def 8
 DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);
correctness
coherence
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #) is DTConstrStr ;
;
end;

:: deftheorem  defines DTConMSA MSAFREE:def_8_:_
 for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds DTConMSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

registration
let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;
cluster DTConMSA X ->  non empty strict ;
coherence
 ( DTConMSA X is strict & not DTConMSA X is empty ) ;
end;

theorem Th6: :: MSAFREE:6
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds
( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S holds
( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )
let X be ManySortedSet of the carrier of S; ::_thesis: ( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )
set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) by LANG1:1;
thus A2: NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] ::_thesis: ( Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NonTerminals (DTConMSA X) or x in [: the carrier' of S,{ the carrier of S}:] )
assume  x in NonTerminals (DTConMSA X) ; ::_thesis: x in [: the carrier' of S,{ the carrier of S}:]
then  x in  {  s where s is Symbol of (DTConMSA X) : ex n being FinSequence st s ==> n  }  by LANG1:def_3;
then consider s being Symbol of (DTConMSA X) such that
A3: s = x and
A4: ex n being FinSequence st s ==> n ;
consider n being FinSequence such that
A5: s ==> n by A4;
 [s,n] in the Rules of (DTConMSA X) by A5, LANG1:def_1;
then reconsider n = n as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
reconsider s = s as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
 [s,n] in REL X by A5, LANG1:def_1;
hence  x in [: the carrier' of S,{ the carrier of S}:] by A3, Def7; ::_thesis: verum
end;
A6: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;
thus A7: Union (coprod X) c= Terminals (DTConMSA X) ::_thesis: ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union (coprod X) or x in Terminals (DTConMSA X) )
assume A8: x in Union (coprod X) ; ::_thesis: x in Terminals (DTConMSA X)
then  x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def_3;
then  ( x in Terminals (DTConMSA X) or x in NonTerminals (DTConMSA X) ) by A1, XBOOLE_0:def_3;
hence  x in Terminals (DTConMSA X) by A6, A2, A8, XBOOLE_0:3; ::_thesis: verum
end;
assume A9: X is V16() ; ::_thesis: ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )
thus  NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] by A2; :: according to XBOOLE_0:def_10 ::_thesis: ( [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConMSA X) & Terminals (DTConMSA X) = Union (coprod X) )
thus A10: [: the carrier' of S,{ the carrier of S}:] c= NonTerminals (DTConMSA X) ::_thesis: Terminals (DTConMSA X) = Union (coprod X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [: the carrier' of S,{ the carrier of S}:] or x in NonTerminals (DTConMSA X) )
assume A11: x in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: x in NonTerminals (DTConMSA X)
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A12: x = [o,x2] by DOMAIN_1:1;
set O = the_arity_of o;
defpred S1[ set , set ] means $2 in coprod (((the_arity_of o) . $1),X);
A13: for a being set st a in Seg (len (the_arity_of o)) holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in Seg (len (the_arity_of o)) implies ex b being set st S1[a,b] )
assume  a in Seg (len (the_arity_of o)) ; ::_thesis: ex b being set st S1[a,b]
then  a in dom (the_arity_of o) by FINSEQ_1:def_3;
then A14: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def_3;
A15: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then consider x being set  such that
A16: x in X . ((the_arity_of o) . a) by A9, A14, XBOOLE_0:def_1;
take  [x,((the_arity_of o) . a)] ; ::_thesis: S1[a,[x,((the_arity_of o) . a)]]
thus  S1[a,[x,((the_arity_of o) . a)]] by A14, A15, A16, Def2; ::_thesis: verum
end;
consider b being Function such that
A17: ( dom b = Seg (len (the_arity_of o)) & ( for a being set st a in Seg (len (the_arity_of o)) holds
S1[a,b . a] ) ) from CLASSES1:sch_1(A13);
reconsider b = b as FinSequence by A17, FINSEQ_1:def_2;
 rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng b or a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) )
A18: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
assume  a in rng b ; ::_thesis: a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
then consider c being set  such that
A19: c in dom b and
A20: b . c = a by FUNCT_1:def_3;
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then A21: (the_arity_of o) . c in rng (the_arity_of o) by A17, A19, FUNCT_1:def_3;
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A21, A18, FUNCT_1:def_3;
then A22: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A21, A18, Def3;
 a in coprod (((the_arity_of o) . c),X) by A17, A19, A20;
then  a in union (rng (coprod X)) by A22, TARSKI:def_4;
then  a in Union (coprod X) by CARD_3:def_4;
hence  a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def_4;
reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def_11;
A23: now__::_thesis:_for_c_being_set_st_c_in_dom_b_holds_
(_(_b_._c_in_[:_the_carrier'_of_S,{_the_carrier_of_S}:]_implies_for_o1_being_OperSymbol_of_S_st_[o1,_the_carrier_of_S]_=_b_._c_holds_
the_result_sort_of_o1_=_(the_arity_of_o)_._c_)_&_(_b_._c_in_Union_(coprod_X)_implies_b_._c_in_coprod_(((the_arity_of_o)_._c),X)_)_)
let c be set ; ::_thesis: ( c in dom b implies ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) ) )
assume A24: c in dom b ; ::_thesis: ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) )
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then A25: (the_arity_of o) . c in rng (the_arity_of o) by A17, A24, FUNCT_1:def_3;
A26: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A25, A26, FUNCT_1:def_3;
then A27: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A25, A26, Def3;
 S1[c,b . c] by A17, A24;
then  b . c in union (rng (coprod X)) by A27, TARSKI:def_4;
then  b . c in Union (coprod X) by CARD_3:def_4;
hence  ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) by A6, XBOOLE_0:3; ::_thesis: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )
assume  b . c in Union (coprod X) ; ::_thesis: b . c in coprod (((the_arity_of o) . c),X)
thus  b . c in coprod (((the_arity_of o) . c),X) by A17, A24; ::_thesis: verum
end;
A28: the carrier of S = x2 by TARSKI:def_1;
then reconsider xa = [o, the carrier of S] as Element of the carrier of (DTConMSA X) by A11, A12, XBOOLE_0:def_3;
 len b = len (the_arity_of o) by A17, FINSEQ_1:def_3;
then  [xa,b] in REL X by A23, Th5;
then  xa ==> b by LANG1:def_1;
then  xa in  {  t where t is Symbol of (DTConMSA X) : ex n being FinSequence st t ==> n  }  ;
hence  x in NonTerminals (DTConMSA X) by A12, A28, LANG1:def_3; ::_thesis: verum
end;
A29: Terminals (DTConMSA X) misses NonTerminals (DTConMSA X) by DTCONSTR:8;
thus  Terminals (DTConMSA X) c= Union (coprod X) :: according to XBOOLE_0:def_10 ::_thesis: Union (coprod X) c= Terminals (DTConMSA X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Terminals (DTConMSA X) or x in Union (coprod X) )
assume  x in Terminals (DTConMSA X) ; ::_thesis: x in Union (coprod X)
then  ( x in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & not x in [: the carrier' of S,{ the carrier of S}:] ) by A1, A29, A10, XBOOLE_0:3, XBOOLE_0:def_3;
hence  x in Union (coprod X) by XBOOLE_0:def_3; ::_thesis: verum
end;
thus  Union (coprod X) c= Terminals (DTConMSA X) by A7; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster DTConMSA X ->  with_terminals with_nonterminals with_useful_nonterminals ;
coherence
 ( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals )
proof
set D = DTConMSA X;
set A = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: Terminals (DTConMSA X) = Union (coprod X) by Th6;
A2: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;
A3: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;
 for nt being Symbol of (DTConMSA X) st nt in NonTerminals (DTConMSA X) holds
ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p
proof
let nt be Symbol of (DTConMSA X); ::_thesis: ( nt in NonTerminals (DTConMSA X) implies ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p )
assume  nt in NonTerminals (DTConMSA X) ; ::_thesis: ex p being FinSequence of TS (DTConMSA X) st nt ==> roots p
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A4: nt = [o,x2] by A2, DOMAIN_1:1;
set O = the_arity_of o;
defpred S1[ set , set ] means X in coprod (((the_arity_of o) . S),X);
A5: for a being set st a in Seg (len (the_arity_of o)) holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in Seg (len (the_arity_of o)) implies ex b being set st S1[a,b] )
assume  a in Seg (len (the_arity_of o)) ; ::_thesis: ex b being set st S1[a,b]
then  a in dom (the_arity_of o) by FINSEQ_1:def_3;
then A6: (the_arity_of o) . a in rng (the_arity_of o) by FUNCT_1:def_3;
A7: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then consider x being set  such that
A8: x in X . ((the_arity_of o) . a) by A6, XBOOLE_0:def_1;
take  [x,((the_arity_of o) . a)] ; ::_thesis: S1[a,[x,((the_arity_of o) . a)]]
thus  S1[a,[x,((the_arity_of o) . a)]] by A6, A7, A8, Def2; ::_thesis: verum
end;
consider b being Function such that
A9: ( dom b = Seg (len (the_arity_of o)) & ( for a being set st a in Seg (len (the_arity_of o)) holds
S1[a,b . a] ) ) from CLASSES1:sch_1(A5);
reconsider b = b as FinSequence by A9, FINSEQ_1:def_2;
A10: rng b c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng b or a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) )
A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
assume  a in rng b ; ::_thesis: a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
then consider c being set  such that
A12: c in dom b and
A13: b . c = a by FUNCT_1:def_3;
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then A14: (the_arity_of o) . c in rng (the_arity_of o) by A9, A12, FUNCT_1:def_3;
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A14, A11, FUNCT_1:def_3;
then A15: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A14, A11, Def3;
 a in coprod (((the_arity_of o) . c),X) by A9, A12, A13;
then  a in union (rng (coprod X)) by A15, TARSKI:def_4;
then  a in Union (coprod X) by CARD_3:def_4;
hence  a in [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by XBOOLE_0:def_3; ::_thesis: verum
end;
then reconsider b = b as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) by FINSEQ_1:def_4;
reconsider b = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def_11;
deffunc H1( set ) ->  set = root-tree (b . S);
consider f being Function such that
A16: ( dom f = dom b & ( for x being set st x in dom b holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider f = f as FinSequence by A9, A16, FINSEQ_1:def_2;
 rng f c= TS (DTConMSA X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in TS (DTConMSA X) )
A17: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
assume  x in rng f ; ::_thesis: x in TS (DTConMSA X)
then consider y being set  such that
A18: y in dom f and
A19: f . y = x by FUNCT_1:def_3;
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then A20: (the_arity_of o) . y in rng (the_arity_of o) by A9, A16, A18, FUNCT_1:def_3;
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) . y) in rng (coprod X) by A20, A17, FUNCT_1:def_3;
then A21: coprod (((the_arity_of o) . y),X) in rng (coprod X) by A20, A17, Def3;
 b . y in rng b by A16, A18, FUNCT_1:def_3;
then reconsider a = b . y as Symbol of (DTConMSA X) by A10;
 S1[y,b . y] by A9, A16, A18;
then  b . y in union (rng (coprod X)) by A21, TARSKI:def_4;
then A22: a in Terminals (DTConMSA X) by A1, CARD_3:def_4;
 x = root-tree (b . y) by A16, A18, A19;
hence  x in TS (DTConMSA X) by A22, DTCONSTR:def_1; ::_thesis: verum
end;
then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def_4;
A23: for x being set st x in dom b holds
(roots f) . x = b . x
proof
let x be set ; ::_thesis: ( x in dom b implies (roots f) . x = b . x )
assume A24: x in dom b ; ::_thesis: (roots f) . x = b . x
then reconsider i = x as Nat ;
 ( f . x = root-tree (b . x) & ex T being DecoratedTree st
( T = f . i & (roots f) . i = T . {} ) ) by A16, A24, TREES_3:def_18;
hence  (roots f) . x = b . x by TREES_4:3; ::_thesis: verum
end;
A25: now__::_thesis:_for_c_being_set_st_c_in_dom_b_holds_
(_(_b_._c_in_[:_the_carrier'_of_S,{_the_carrier_of_S}:]_implies_for_o1_being_OperSymbol_of_S_st_[o1,_the_carrier_of_S]_=_b_._c_holds_
the_result_sort_of_o1_=_(the_arity_of_o)_._c_)_&_(_b_._c_in_Union_(coprod_X)_implies_b_._c_in_coprod_(((the_arity_of_o)_._c),X)_)_)
let c be set ; ::_thesis: ( c in dom b implies ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) ) )
assume A26: c in dom b ; ::_thesis: ( ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) & ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) ) )
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then A27: (the_arity_of o) . c in rng (the_arity_of o) by A9, A26, FUNCT_1:def_3;
A28: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) . c) in rng (coprod X) by A27, A28, FUNCT_1:def_3;
then A29: coprod (((the_arity_of o) . c),X) in rng (coprod X) by A27, A28, Def3;
 S1[c,b . c] by A9, A26;
then  b . c in union (rng (coprod X)) by A29, TARSKI:def_4;
then  b . c in Union (coprod X) by CARD_3:def_4;
hence  ( b . c in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . c holds
the_result_sort_of o1 = (the_arity_of o) . c ) by A3, XBOOLE_0:3; ::_thesis: ( b . c in Union (coprod X) implies b . c in coprod (((the_arity_of o) . c),X) )
assume  b . c in Union (coprod X) ; ::_thesis: b . c in coprod (((the_arity_of o) . c),X)
thus  b . c in coprod (((the_arity_of o) . c),X) by A9, A26; ::_thesis: verum
end;
 ( the carrier of S = x2 & len b = len (the_arity_of o) ) by A9, FINSEQ_1:def_3, TARSKI:def_1;
then  [nt,b] in REL X by A4, A25, Th5;
then A30: nt ==> b by LANG1:def_1;
take  f ; ::_thesis: nt ==> roots f
 dom (roots f) = dom f by TREES_3:def_18;
hence  nt ==> roots f by A30, A16, A23, FUNCT_1:2; ::_thesis: verum
end;
hence  ( DTConMSA X is with_terminals & DTConMSA X is with_nonterminals & DTConMSA X is with_useful_nonterminals ) by A1, A2, DTCONSTR:def_3, DTCONSTR:def_4, DTCONSTR:def_5; ::_thesis: verum
end;
end;

theorem Th7: :: MSAFREE:7
for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
let X be ManySortedSet of the carrier of S; ::_thesis: for t being set holds
( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
let t be set ; ::_thesis: ( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
set D = DTConMSA X;
A1: Union (coprod X) c= Terminals (DTConMSA X) by Th6;
A2: Union (coprod X) = union (rng (coprod X)) by CARD_3:def_4;
thus  ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) ::_thesis: for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X)
proof
assume that
A3: t in Terminals (DTConMSA X) and
A4: X is V16() ; ::_thesis: ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] )
 Terminals (DTConMSA X) = Union (coprod X) by A4, Th6;
then consider A being set  such that
A5: t in A and
A6: A in rng (coprod X) by A2, A3, TARSKI:def_4;
consider s being set  such that
A7: s in dom (coprod X) and
A8: (coprod X) . s = A by A6, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A7;
 (coprod X) . s = coprod (s,X) by Def3;
then consider x being set  such that
A9: ( x in X . s & t = [x,s] ) by A5, A8, Def2;
take  s ; ::_thesis: ex x being set st
( x in X . s & t = [x,s] )
take  x ; ::_thesis: ( x in X . s & t = [x,s] )
thus  ( x in X . s & t = [x,s] ) by A9; ::_thesis: verum
end;
let s be SortSymbol of S; ::_thesis: for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X)
let x be set ; ::_thesis: ( x in X . s implies [x,s] in Terminals (DTConMSA X) )
assume A10: x in X . s ; ::_thesis: [x,s] in Terminals (DTConMSA X)
set t = [x,s];
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then A11: (coprod X) . s in rng (coprod X) by FUNCT_1:def_3;
 [x,s] in coprod (s,X) by A10, Def2;
then  [x,s] in (coprod X) . s by Def3;
then  [x,s] in Union (coprod X) by A2, A11, TARSKI:def_4;
hence  [x,s] in Terminals (DTConMSA X) by A1; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
func Sym (o,X) ->  Symbol of (DTConMSA X) equals :: MSAFREE:def 9
[o, the carrier of S];
coherence
 [o, the carrier of S] is Symbol of (DTConMSA X)
proof
 the carrier of S in { the carrier of S} by TARSKI:def_1;
then  [o, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
then  [o, the carrier of S] in NonTerminals (DTConMSA X) by Th6;
hence  [o, the carrier of S] is Symbol of (DTConMSA X) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Sym MSAFREE:def_9_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S holds Sym (o,X) = [o, the carrier of S];

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeSort (X,s) ->  Subset of (TS (DTConMSA X)) equals :: MSAFREE:def 10
 {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  ;
coherence
  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  is Subset of (TS (DTConMSA X))
proof
set A =  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  ;
  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  c= TS (DTConMSA X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  or x in TS (DTConMSA X) )
assume  x in  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  ; ::_thesis: x in TS (DTConMSA X)
then  ex a being Element of TS (DTConMSA X) st
( x = a & ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) ) ;
hence  x in TS (DTConMSA X) ; ::_thesis: verum
end;
hence   {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  is Subset of (TS (DTConMSA X)) ; ::_thesis: verum
end;
end;

:: deftheorem  defines FreeSort MSAFREE:def_10_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (X,s) =  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  ;

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeSort (X,s) ->  non empty ;
coherence
 not FreeSort (X,s) is empty
proof
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . s in rng (coprod X) by FUNCT_1:def_3;
then A1: coprod (s,X) in rng (coprod X) by Def3;
set A =  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  ;
consider x being set  such that
A2: x in X . s by XBOOLE_0:def_1;
set a = [x,s];
A3: Terminals (DTConMSA X) = Union (coprod X) by Th6;
 [x,s] in coprod (s,X) by A2, Def2;
then  [x,s] in union (rng (coprod X)) by A1, TARSKI:def_4;
then A4: [x,s] in Terminals (DTConMSA X) by A3, CARD_3:def_4;
then reconsider a = [x,s] as Symbol of (DTConMSA X) ;
reconsider b = root-tree a as Element of TS (DTConMSA X) by A4, DTCONSTR:def_1;
 b in  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) )  }  by A2;
hence  not FreeSort (X,s) is empty ; ::_thesis: verum
end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeSort X ->  ManySortedSet of the carrier of S means :Def11: :: MSAFREE:def 11
 for s being SortSymbol of S holds it . s = FreeSort (X,s);
existence
 ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = FreeSort (X,s)
proof
deffunc H1( Element of S) ->  Subset of (TS (DTConMSA X)) = FreeSort (X,$1);
consider f being Function such that
A1: ( dom f = the carrier of S & ( for d being Element of S holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
take  f ; ::_thesis: for s being SortSymbol of S holds f . s = FreeSort (X,s)
thus  for s being SortSymbol of S holds f . s = FreeSort (X,s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = FreeSort (X,s) ) & ( for s being SortSymbol of S holds b2 . s = FreeSort (X,s) ) holds
b1 = b2
proof
let A, B be ManySortedSet of the carrier of S; ::_thesis: ( ( for s being SortSymbol of S holds A . s = FreeSort (X,s) ) & ( for s being SortSymbol of S holds B . s = FreeSort (X,s) ) implies A = B )
assume that
A2: for s being SortSymbol of S holds A . s = FreeSort (X,s) and
A3: for s being SortSymbol of S holds B . s = FreeSort (X,s) ; ::_thesis: A = B
 for i being set st i in the carrier of S holds
A . i = B . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies A . i = B . i )
assume  i in the carrier of S ; ::_thesis: A . i = B . i
then reconsider s = i as SortSymbol of S ;
 A . s = FreeSort (X,s) by A2;
hence  A . i = B . i by A3; ::_thesis: verum
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def11 defines FreeSort MSAFREE:def_11_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedSet of the carrier of S holds
( b3 = FreeSort X iff for s being SortSymbol of S holds b3 . s = FreeSort (X,s) );

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeSort X -> V16() ;
coherence
 FreeSort X is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in the carrier of S or not (FreeSort X) . i is empty )
assume  i in the carrier of S ; ::_thesis: not (FreeSort X) . i is empty
then reconsider s = i as SortSymbol of S ;
 (FreeSort X) . s = FreeSort (X,s) by Def11;
hence  not (FreeSort X) . i is empty ; ::_thesis: verum
end;
end;

theorem Th8: :: MSAFREE:8
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let X be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let o be OperSymbol of S; ::_thesis: for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)
let x be set ; ::_thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies x is FinSequence of TS (DTConMSA X) )
set D = DTConMSA X;
set ar = the_arity_of o;
set cr = the carrier of S;
A1: the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
 ( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
then A2: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
assume  x in (((FreeSort X) #) * the Arity of S) . o ; ::_thesis: x is FinSequence of TS (DTConMSA X)
then  x in product ((FreeSort X) * (the_arity_of o)) by A1, Th1;
then consider f being Function such that
A3: x = f and
A4: dom f = dom ((FreeSort X) * (the_arity_of o)) and
A5: for y being set st y in dom ((FreeSort X) * (the_arity_of o)) holds
f . y in ((FreeSort X) * (the_arity_of o)) . y by CARD_3:def_5;
 dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3;
then reconsider f = f as FinSequence by A4, A2, FINSEQ_1:def_2;
 rng f c= TS (DTConMSA X)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in TS (DTConMSA X) )
assume  a in rng f ; ::_thesis: a in TS (DTConMSA X)
then consider b being set  such that
A6: b in dom f and
A7: f . b = a by FUNCT_1:def_3;
A8: a in ((FreeSort X) * (the_arity_of o)) . b by A4, A5, A6, A7;
reconsider b = b as Nat by A6;
((FreeSort X) * (the_arity_of o)) . b = (FreeSort X) . ((the_arity_of o) . b) by A4, A6, FUNCT_1:12
.= (FreeSort X) . ((the_arity_of o) /. b) by A4, A2, A6, PARTFUN1:def_6
.= FreeSort (X,((the_arity_of o) /. b)) by Def11
.=  {  s where s is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. b) & s = root-tree [x,((the_arity_of o) /. b)] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = s . {} & the_result_sort_of o1 = (the_arity_of o) /. b ) )  }  ;
then  ex e being Element of TS (DTConMSA X) st
( a = e & ( ex x being set st
( x in X . ((the_arity_of o) /. b) & e = root-tree [x,((the_arity_of o) /. b)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = e . {} & the_result_sort_of o = (the_arity_of o) /. b ) ) ) by A8;
hence  a in TS (DTConMSA X) ; ::_thesis: verum
end;
then reconsider f = f as FinSequence of TS (DTConMSA X) by FINSEQ_1:def_4;
 f = x by A3;
hence  x is FinSequence of TS (DTConMSA X) ; ::_thesis: verum
end;

theorem Th9: :: MSAFREE:9
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let X be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let o be OperSymbol of S; ::_thesis: for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
let p be FinSequence of TS (DTConMSA X); ::_thesis: ( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )
set AR = the Arity of S;
set cr = the carrier of S;
set ar = the_arity_of o;
thus  ( p in (((FreeSort X) #) * the Arity of S) . o implies ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) ) ::_thesis: ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) implies p in (((FreeSort X) #) * the Arity of S) . o )
proof
A1: the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
A2: ( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
then A3: dom ((FreeSort X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
assume  p in (((FreeSort X) #) * the Arity of S) . o ; ::_thesis: ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) )
then A4: p in product ((FreeSort X) * (the_arity_of o)) by A1, Th1;
then A5: dom p = dom ((FreeSort X) * (the_arity_of o)) by CARD_3:9;
hence  dom p = dom (the_arity_of o) by A2, RELAT_1:27; ::_thesis: for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n))
let n be Nat; ::_thesis: ( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )
assume A6: n in dom p ; ::_thesis: p . n in FreeSort (X,((the_arity_of o) /. n))
then ((FreeSort X) * (the_arity_of o)) . n = (FreeSort X) . ((the_arity_of o) . n) by A5, FUNCT_1:12
.= (FreeSort X) . ((the_arity_of o) /. n) by A5, A3, A6, PARTFUN1:def_6
.= FreeSort (X,((the_arity_of o) /. n)) by Def11 ;
hence  p . n in FreeSort (X,((the_arity_of o) /. n)) by A4, A5, A6, CARD_3:9; ::_thesis: verum
end;
assume that
A7: dom p = dom (the_arity_of o) and
A8: for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ; ::_thesis: p in (((FreeSort X) #) * the Arity of S) . o
 ( rng (the_arity_of o) c= the carrier of S & dom (FreeSort X) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
then A9: dom p = dom ((FreeSort X) * (the_arity_of o)) by A7, RELAT_1:27;
A10: for x being set st x in dom ((FreeSort X) * (the_arity_of o)) holds
p . x in ((FreeSort X) * (the_arity_of o)) . x
proof
let x be set ; ::_thesis: ( x in dom ((FreeSort X) * (the_arity_of o)) implies p . x in ((FreeSort X) * (the_arity_of o)) . x )
assume A11: x in dom ((FreeSort X) * (the_arity_of o)) ; ::_thesis: p . x in ((FreeSort X) * (the_arity_of o)) . x
then reconsider n = x as Nat ;
FreeSort (X,((the_arity_of o) /. n)) = (FreeSort X) . ((the_arity_of o) /. n) by Def11
.= (FreeSort X) . ((the_arity_of o) . n) by A7, A9, A11, PARTFUN1:def_6
.= ((FreeSort X) * (the_arity_of o)) . x by A11, FUNCT_1:12 ;
hence  p . x in ((FreeSort X) * (the_arity_of o)) . x by A8, A9, A11; ::_thesis: verum
end;
 the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
then  (((FreeSort X) #) * the Arity of S) . o = product ((FreeSort X) * (the_arity_of o)) by Th1;
hence  p in (((FreeSort X) #) * the Arity of S) . o by A9, A10, CARD_3:9; ::_thesis: verum
end;

theorem Th10: :: MSAFREE:10
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let X be V16() ManySortedSet of the carrier of S; ::_thesis: for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let o be OperSymbol of S; ::_thesis: for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
let p be FinSequence of TS (DTConMSA X); ::_thesis: ( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )
set D = DTConMSA X;
set ar = the_arity_of o;
set r = roots p;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
A1: dom p = dom (roots p) by TREES_3:def_18;
thus  ( Sym (o,X) ==> roots p implies p in (((FreeSort X) #) * the Arity of S) . o ) ::_thesis: ( p in (((FreeSort X) #) * the Arity of S) . o implies Sym (o,X) ==> roots p )
proof
assume  Sym (o,X) ==> roots p ; ::_thesis: p in (((FreeSort X) #) * the Arity of S) . o
then A2: [[o, the carrier of S],(roots p)] in REL X by LANG1:def_1;
then reconsider r = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def_18;
A4: ( dom r = Seg (len r) & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def_3;
A5: len r = len (the_arity_of o) by A2, Th5;
 for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n))
proof
let n be Nat; ::_thesis: ( n in dom p implies p . n in FreeSort (X,((the_arity_of o) /. n)) )
set s = (the_arity_of o) /. n;
assume A6: n in dom p ; ::_thesis: p . n in FreeSort (X,((the_arity_of o) /. n))
then consider T being DecoratedTree such that
A7: T = p . n and
A8: r . n = T . {} by TREES_3:def_18;
 ( rng p c= TS (DTConMSA X) & p . n in rng p ) by A6, FINSEQ_1:def_4, FUNCT_1:def_3;
then reconsider T = T as Element of TS (DTConMSA X) by A7;
A9: ( rng r c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & r . n in rng r ) by A3, A6, FINSEQ_1:def_4, FUNCT_1:def_3;
percases ( r . n in [: the carrier' of S,{ the carrier of S}:] or r . n in Union (coprod X) ) by A9, XBOOLE_0:def_3;
supposeA10: r . n in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: p . n in FreeSort (X,((the_arity_of o) /. n))
then consider o1 being OperSymbol of S, x2 being Element of { the carrier of S} such that
A11: r . n = [o1,x2] by DOMAIN_1:1;
A12: x2 = the carrier of S by TARSKI:def_1;
then  the_result_sort_of o1 = (the_arity_of o) . n by A2, A3, A6, A10, A11, Th5
.= (the_arity_of o) /. n by A5, A3, A4, A6, PARTFUN1:def_6 ;
then  ( ex x being set st
( x in X . ((the_arity_of o) /. n) & T = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = T . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) by A8, A11, A12;
hence  p . n in FreeSort (X,((the_arity_of o) /. n)) by A7; ::_thesis: verum
end;
supposeA13: r . n in Union (coprod X) ; ::_thesis: p . n in FreeSort (X,((the_arity_of o) /. n))
then  r . n in coprod (((the_arity_of o) . n),X) by A2, A3, A6, Th5;
then  r . n in coprod (((the_arity_of o) /. n),X) by A5, A3, A4, A6, PARTFUN1:def_6;
then A14: ex a being set st
( a in X . ((the_arity_of o) /. n) & r . n = [a,((the_arity_of o) /. n)] ) by Def2;
reconsider t = r . n as Terminal of (DTConMSA X) by A13, Th6;
 T = root-tree t by A8, DTCONSTR:9;
hence  p . n in FreeSort (X,((the_arity_of o) /. n)) by A7, A14; ::_thesis: verum
end;
end;
end;
hence  p in (((FreeSort X) #) * the Arity of S) . o by A5, A3, A4, Th9; ::_thesis: verum
end;
A15: dom (roots p) = Seg (len (roots p)) by FINSEQ_1:def_3;
reconsider r = roots p as FinSequence of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
reconsider r = r as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by FINSEQ_1:def_11;
assume A16: p in (((FreeSort X) #) * the Arity of S) . o ; ::_thesis: Sym (o,X) ==> roots p
then A17: dom p = dom (the_arity_of o) by Th9;
A18: Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:] by Th4;
A19: for x being set st x in dom r holds
( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( r . x in Union (coprod X) implies r . x in coprod (((the_arity_of o) . x),X) ) )
proof
let x be set ; ::_thesis: ( x in dom r implies ( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( r . x in Union (coprod X) implies r . x in coprod (((the_arity_of o) . x),X) ) ) )
assume A20: x in dom r ; ::_thesis: ( ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( r . x in Union (coprod X) implies r . x in coprod (((the_arity_of o) . x),X) ) )
then reconsider n = x as Nat ;
A21: ex T being DecoratedTree st
( T = p . n & r . n = T . {} ) by A1, A20, TREES_3:def_18;
set s = (the_arity_of o) /. n;
 p . n in FreeSort (X,((the_arity_of o) /. n)) by A16, A1, A20, Th9;
then consider a being Element of TS (DTConMSA X) such that
A22: a = p . n and
A23: ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) ;
A24: (the_arity_of o) /. n = (the_arity_of o) . n by A17, A1, A20, PARTFUN1:def_6;
thus  ( r . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) ::_thesis: ( r . x in Union (coprod X) implies r . x in coprod (((the_arity_of o) . x),X) )
proof
assume A25: r . x in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: for o1 being OperSymbol of S st [o1, the carrier of S] = r . x holds
the_result_sort_of o1 = (the_arity_of o) . x
A26: now__::_thesis:_for_y_being_set_holds_
(_not_y_in_X_._((the_arity_of_o)_/._n)_or_not_a_=_root-tree_[y,((the_arity_of_o)_/._n)]_)
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . ((the_arity_of o) /. n) in rng (coprod X) by FUNCT_1:def_3;
then A27: coprod (((the_arity_of o) /. n),X) in rng (coprod X) by Def3;
given y being set  such that A28: ( y in X . ((the_arity_of o) /. n) & a = root-tree [y,((the_arity_of o) /. n)] ) ; ::_thesis: contradiction
 ( r . x = [y,((the_arity_of o) /. n)] & [y,((the_arity_of o) /. n)] in coprod (((the_arity_of o) /. n),X) ) by A22, A21, A28, Def2, TREES_4:3;
then  r . x in union (rng (coprod X)) by A27, TARSKI:def_4;
then  r . x in Union (coprod X) by CARD_3:def_4;
hence  contradiction by A18, A25, XBOOLE_0:3; ::_thesis: verum
end;
let o1 be OperSymbol of S; ::_thesis: ( [o1, the carrier of S] = r . x implies the_result_sort_of o1 = (the_arity_of o) . x )
assume  [o1, the carrier of S] = r . x ; ::_thesis: the_result_sort_of o1 = (the_arity_of o) . x
hence  the_result_sort_of o1 = (the_arity_of o) . x by A22, A23, A21, A24, A26, XTUPLE_0:1; ::_thesis: verum
end;
assume A29: r . x in Union (coprod X) ; ::_thesis: r . x in coprod (((the_arity_of o) . x),X)
now__::_thesis:_for_o1_being_OperSymbol_of_S_holds_
(_not_[o1,_the_carrier_of_S]_=_a_._{}_or_not_the_result_sort_of_o1_=_(the_arity_of_o)_/._n_)
given o1 being OperSymbol of S such that A30: [o1, the carrier of S] = a . {} and
 the_result_sort_of o1 = (the_arity_of o) /. n ; ::_thesis: contradiction
 the carrier of S in { the carrier of S} by TARSKI:def_1;
then  [o1, the carrier of S] in [: the carrier' of S,{ the carrier of S}:] by ZFMISC_1:87;
hence  contradiction by A18, A22, A21, A29, A30, XBOOLE_0:3; ::_thesis: verum
end;
then consider y being set  such that
A31: y in X . ((the_arity_of o) /. n) and
A32: a = root-tree [y,((the_arity_of o) /. n)] by A23;
 r . x = [y,((the_arity_of o) /. n)] by A22, A21, A32, TREES_4:3;
hence  r . x in coprod (((the_arity_of o) . x),X) by A24, A31, Def2; ::_thesis: verum
end;
 len r = len (the_arity_of o) by A17, A1, A15, FINSEQ_1:def_3;
then  [[o, the carrier of S],r] in REL X by A19, Th5;
hence  Sym (o,X) ==> roots p by LANG1:def_1; ::_thesis: verum
end;

theorem Th11: :: MSAFREE:11
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)
let X be V16() ManySortedSet of the carrier of S; ::_thesis: union (rng (FreeSort X)) = TS (DTConMSA X)
set D = DTConMSA X;
A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def_2;
thus  union (rng (FreeSort X)) c= TS (DTConMSA X) :: according to XBOOLE_0:def_10 ::_thesis: TS (DTConMSA X) c= union (rng (FreeSort X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng (FreeSort X)) or x in TS (DTConMSA X) )
assume  x in union (rng (FreeSort X)) ; ::_thesis: x in TS (DTConMSA X)
then consider A being set  such that
A2: x in A and
A3: A in rng (FreeSort X) by TARSKI:def_4;
consider s being set  such that
A4: s in dom (FreeSort X) and
A5: (FreeSort X) . s = A by A3, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A4;
A = FreeSort (X,s) by A5, Def11
.=  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) )  }  ;
then  ex a being Element of TS (DTConMSA X) st
( a = x & ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A2;
hence  x in TS (DTConMSA X) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TS (DTConMSA X) or x in union (rng (FreeSort X)) )
assume  x in TS (DTConMSA X) ; ::_thesis: x in union (rng (FreeSort X))
then reconsider t = x as Element of TS (DTConMSA X) ;
A6: ( rng t c= the carrier of (DTConMSA X) & the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) ) by LANG1:1, RELAT_1:def_19;
 {} in dom t by TREES_1:22;
then A7: t . {} in rng t by FUNCT_1:def_3;
A8: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;
A9: Terminals (DTConMSA X) = Union (coprod X) by Th6;
percases ( t . {} in Terminals (DTConMSA X) or t . {} in NonTerminals (DTConMSA X) ) by A7, A6, XBOOLE_0:def_3;
supposeA10: t . {} in Terminals (DTConMSA X) ; ::_thesis: x in union (rng (FreeSort X))
then reconsider a = t . {} as Terminal of (DTConMSA X) ;
 a in union (rng (coprod X)) by A9, A10, CARD_3:def_4;
then consider A being set  such that
A11: a in A and
A12: A in rng (coprod X) by TARSKI:def_4;
consider s being set  such that
A13: s in dom (coprod X) and
A14: (coprod X) . s = A by A12, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A13;
 A = coprod (s,X) by A14, Def3;
then  ( t = root-tree a & ex b being set st
( b in X . s & a = [b,s] ) ) by A11, Def2, DTCONSTR:9;
then  t in FreeSort (X,s) ;
then A15: t in (FreeSort X) . s by Def11;
 (FreeSort X) . s in rng (FreeSort X) by A1, FUNCT_1:def_3;
hence  x in union (rng (FreeSort X)) by A15, TARSKI:def_4; ::_thesis: verum
end;
suppose t . {} in NonTerminals (DTConMSA X) ; ::_thesis: x in union (rng (FreeSort X))
then reconsider a = t . {} as NonTerminal of (DTConMSA X) ;
consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A16: a = [o,x2] by A8, DOMAIN_1:1;
set rs = the_result_sort_of o;
 x2 = the carrier of S by TARSKI:def_1;
then  t in FreeSort (X,(the_result_sort_of o)) by A16;
then A17: t in (FreeSort X) . (the_result_sort_of o) by Def11;
 (FreeSort X) . (the_result_sort_of o) in rng (FreeSort X) by A1, FUNCT_1:def_3;
hence  x in union (rng (FreeSort X)) by A17, TARSKI:def_4; ::_thesis: verum
end;
end;
end;

theorem Th12: :: MSAFREE:12
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
let X be V16() ManySortedSet of the carrier of S; ::_thesis: for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2
let s1, s2 be SortSymbol of S; ::_thesis: ( s1 <> s2 implies (FreeSort X) . s1 misses (FreeSort X) . s2 )
assume that
A1: s1 <> s2 and
A2: ((FreeSort X) . s1) /\ ((FreeSort X) . s2) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
consider x being set  such that
A3: x in ((FreeSort X) . s1) /\ ((FreeSort X) . s2) by A2, XBOOLE_0:def_1;
set D = DTConMSA X;
A4: (FreeSort X) . s1 = FreeSort (X,s1) by Def11;
A5: (FreeSort X) . s2 = FreeSort (X,s2) by Def11;
 x in (FreeSort X) . s2 by A3, XBOOLE_0:def_4;
then consider b being Element of TS (DTConMSA X) such that
A6: b = x and
A7: ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A5;
 x in (FreeSort X) . s1 by A3, XBOOLE_0:def_4;
then consider a being Element of TS (DTConMSA X) such that
A8: a = x and
A9: ( ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s1 ) ) by A4;
percases ( ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s1 ) ) by A9;
suppose ex x1 being set st
( x1 in X . s1 & a = root-tree [x1,s1] ) ; ::_thesis: contradiction
then consider x1 being set  such that
 x1 in X . s1 and
A10: a = root-tree [x1,s1] ;
now__::_thesis:_(_(_ex_x2_being_set_st_
(_x2_in_X_._s2_&_b_=_root-tree_[x2,s2]_)_&_contradiction_)_or_(_ex_o2_being_OperSymbol_of_S_st_
(_[o2,_the_carrier_of_S]_=_b_._{}_&_the_result_sort_of_o2_=_s2_)_&_contradiction_)_)
percases ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A7;
case ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) ; ::_thesis: contradiction
then consider x2 being set  such that
 x2 in X . s2 and
A11: b = root-tree [x2,s2] ;
 [x1,s1] = [x2,s2] by A8, A6, A10, A11, TREES_4:4;
hence  contradiction by A1, XTUPLE_0:1; ::_thesis: verum
end;
case ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ; ::_thesis: contradiction
then consider o2 being OperSymbol of S such that
A12: [o2, the carrier of S] = b . {} and
 the_result_sort_of o2 = s2 ;
 [o2, the carrier of S] = [x1,s1] by A8, A6, A10, A12, TREES_4:3;
then A13: the carrier of S = s1 by XTUPLE_0:1;
 for X being set holds not X in X ;
hence  contradiction by A13; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
suppose ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s1 ) ; ::_thesis: contradiction
then consider o1 being OperSymbol of S such that
A14: [o1, the carrier of S] = a . {} and
A15: the_result_sort_of o1 = s1 ;
now__::_thesis:_(_(_ex_x2_being_set_st_
(_x2_in_X_._s2_&_b_=_root-tree_[x2,s2]_)_&_contradiction_)_or_(_ex_o2_being_OperSymbol_of_S_st_
(_[o2,_the_carrier_of_S]_=_b_._{}_&_the_result_sort_of_o2_=_s2_)_&_contradiction_)_)
percases ( ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) or ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ) by A7;
case ex x2 being set st
( x2 in X . s2 & b = root-tree [x2,s2] ) ; ::_thesis: contradiction
then consider x2 being set  such that
 x2 in X . s2 and
A16: b = root-tree [x2,s2] ;
 [o1, the carrier of S] = [x2,s2] by A8, A6, A14, A16, TREES_4:3;
then A17: the carrier of S = s2 by XTUPLE_0:1;
 for X being set holds not X in X ;
hence  contradiction by A17; ::_thesis: verum
end;
case ex o2 being OperSymbol of S st
( [o2, the carrier of S] = b . {} & the_result_sort_of o2 = s2 ) ; ::_thesis: contradiction
hence  contradiction by A1, A8, A6, A14, A15, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
end;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
func DenOp (o,X) ->  Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) means :Def12: :: MSAFREE:def 12
 for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
it . p = (Sym (o,X)) -tree p;
existence
 ex b1 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st
for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p
proof
set AL = (((FreeSort X) #) * the Arity of S) . o;
set AX = ((FreeSort X) * the ResultSort of S) . o;
set D = DTConMSA X;
set O = the carrier' of S;
set rs = the_result_sort_of o;
set RS = the ResultSort of S;
defpred S1[ set , set ] means  for p being FinSequence of TS (DTConMSA X) st p = $1 holds
$2 = (Sym (o,X)) -tree p;
A1: for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] ) )
assume A2: x in (((FreeSort X) #) * the Arity of S) . o ; ::_thesis: ex y being set st
( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;
 Sym (o,X) ==> roots p by A2, Th10;
then reconsider a = (Sym (o,X)) -tree p as Element of TS (DTConMSA X) by DTCONSTR:def_1;
take y = (Sym (o,X)) -tree p; ::_thesis: ( y in ((FreeSort X) * the ResultSort of S) . o & S1[x,y] )
 o in the carrier' of S ;
then  o in dom ((FreeSort X) * the ResultSort of S) by PARTFUN1:def_2;
then A3: ((FreeSort X) * the ResultSort of S) . o = (FreeSort X) . ( the ResultSort of S . o) by FUNCT_1:12
.= (FreeSort X) . (the_result_sort_of o) by MSUALG_1:def_2
.= FreeSort (X,(the_result_sort_of o)) by Def11 ;
 a . {} = Sym (o,X) by TREES_4:def_4;
hence  y in ((FreeSort X) * the ResultSort of S) . o by A3; ::_thesis: S1[x,y]
thus  S1[x,y] ; ::_thesis: verum
end;
consider f being Function such that
A4: ( dom f = (((FreeSort X) #) * the Arity of S) . o & rng f c= ((FreeSort X) * the ResultSort of S) . o & ( for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider g = f as Function of ((((FreeSort X) #) * the Arity of S) . o),(rng f) by A4, FUNCT_2:1;
reconsider g = g as Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) by A4, FUNCT_2:2;
take  g ; ::_thesis: for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p
let p be FinSequence of TS (DTConMSA X); ::_thesis: ( Sym (o,X) ==> roots p implies g . p = (Sym (o,X)) -tree p )
assume  Sym (o,X) ==> roots p ; ::_thesis: g . p = (Sym (o,X)) -tree p
then  p in (((FreeSort X) #) * the Arity of S) . o by Th10;
hence  g . p = (Sym (o,X)) -tree p by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b1 . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b2 . p = (Sym (o,X)) -tree p ) holds
b1 = b2
proof
set AL = (((FreeSort X) #) * the Arity of S) . o;
set AX = ((FreeSort X) * the ResultSort of S) . o;
set D = DTConMSA X;
let f, g be Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o); ::_thesis: ( ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p ) implies f = g )
assume that
A5: for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
f . p = (Sym (o,X)) -tree p and
A6: for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
g . p = (Sym (o,X)) -tree p ; ::_thesis: f = g
A7: for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in (((FreeSort X) #) * the Arity of S) . o implies f . x = g . x )
assume A8: x in (((FreeSort X) #) * the Arity of S) . o ; ::_thesis: f . x = g . x
then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;
A9: Sym (o,X) ==> roots p by A8, Th10;
then  f . p = (Sym (o,X)) -tree p by A5;
hence  f . x = g . x by A6, A9; ::_thesis: verum
end;
 ( dom f = (((FreeSort X) #) * the Arity of S) . o & dom g = (((FreeSort X) #) * the Arity of S) . o ) by FUNCT_2:def_1;
hence  f = g by A7, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def12 defines DenOp MSAFREE:def_12_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for b4 being Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) holds
( b4 = DenOp (o,X) iff for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
b4 . p = (Sym (o,X)) -tree p );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeOper X ->  ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S means :Def13: :: MSAFREE:def 13
 for o being OperSymbol of S holds it . o = DenOp (o,X);
existence
 ex b1 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = DenOp (o,X)
proof
defpred S1[ set , set ] means  for o being OperSymbol of S st $1 = o holds
$2 = DenOp (o,X);
set Y = the carrier' of S;
A1: for x being set st x in the carrier' of S holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies ex y being set st S1[x,y] )
assume  x in the carrier' of S ; ::_thesis: ex y being set st S1[x,y]
then reconsider o = x as OperSymbol of S ;
take  DenOp (o,X) ; ::_thesis: S1[x, DenOp (o,X)]
thus  S1[x, DenOp (o,X)] ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = the carrier' of S & ( for x being set st x in the carrier' of S holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
reconsider f = f as ManySortedSet of the carrier' of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume  x in dom f ; ::_thesis: f . x is Function
then reconsider o = x as OperSymbol of S ;
 f . o = DenOp (o,X) by A2;
hence  f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier' of S by FUNCOP_1:def_6;
 for x being set st x in the carrier' of S holds
f . x is Function of ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x)
proof
let x be set ; ::_thesis: ( x in the carrier' of S implies f . x is Function of ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x) )
assume  x in the carrier' of S ; ::_thesis: f . x is Function of ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x)
then reconsider o = x as OperSymbol of S ;
 f . o = DenOp (o,X) by A2;
hence  f . x is Function of ((((FreeSort X) #) * the Arity of S) . x),(((FreeSort X) * the ResultSort of S) . x) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S by PBOOLE:def_15;
take  f ; ::_thesis: for o being OperSymbol of S holds f . o = DenOp (o,X)
let o be OperSymbol of S; ::_thesis: f . o = DenOp (o,X)
thus  f . o = DenOp (o,X) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = DenOp (o,X) ) & ( for o being OperSymbol of S holds b2 . o = DenOp (o,X) ) holds
b1 = b2
proof
let A, B be ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S; ::_thesis: ( ( for o being OperSymbol of S holds A . o = DenOp (o,X) ) & ( for o being OperSymbol of S holds B . o = DenOp (o,X) ) implies A = B )
assume that
A3: for o being OperSymbol of S holds A . o = DenOp (o,X) and
A4: for o being OperSymbol of S holds B . o = DenOp (o,X) ; ::_thesis: A = B
 for i being set st i in the carrier' of S holds
A . i = B . i
proof
let i be set ; ::_thesis: ( i in the carrier' of S implies A . i = B . i )
assume  i in the carrier' of S ; ::_thesis: A . i = B . i
then reconsider s = i as OperSymbol of S ;
 A . s = DenOp (s,X) by A3;
hence  A . i = B . i by A4; ::_thesis: verum
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines FreeOper MSAFREE:def_13_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S holds
( b3 = FreeOper X iff for o being OperSymbol of S holds b3 . o = DenOp (o,X) );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeMSA X ->  MSAlgebra over S equals :: MSAFREE:def 14
 MSAlgebra(# (FreeSort X),(FreeOper X) #);
coherence
 MSAlgebra(# (FreeSort X),(FreeOper X) #) is MSAlgebra over S ;
end;

:: deftheorem  defines FreeMSA MSAFREE:def_14_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #);

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
cluster FreeMSA X ->  strict non-empty ;
coherence
 ( FreeMSA X is strict & FreeMSA X is non-empty ) by MSUALG_1:def_3;
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func FreeGen (s,X) ->  Subset of ((FreeSort X) . s) means :Def15: :: MSAFREE:def 15
 for x being set holds
( x in it iff ex a being set st
( a in X . s & x = root-tree [a,s] ) );
existence
 ex b1 being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) )
proof
defpred S1[ set ] means  ex a being set st
( a in X . s & $1 = root-tree [a,s] );
set D = DTConMSA X;
consider A being set  such that
A1: for x being set holds
( x in A iff ( x in (FreeSort X) . s & S1[x] ) ) from XBOOLE_0:sch_1();
 A c= (FreeSort X) . s
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (FreeSort X) . s )
assume  x in A ; ::_thesis: x in (FreeSort X) . s
hence  x in (FreeSort X) . s by A1; ::_thesis: verum
end;
then reconsider A = A as Subset of ((FreeSort X) . s) ;
 for x being set holds
( x in A iff S1[x] )
proof
 dom (coprod X) = the carrier of S by PARTFUN1:def_2;
then  (coprod X) . s in rng (coprod X) by FUNCT_1:def_3;
then A2: coprod (s,X) in rng (coprod X) by Def3;
A3: Terminals (DTConMSA X) = Union (coprod X) by Th6;
let x be set ; ::_thesis: ( x in A iff S1[x] )
thus  ( x in A implies S1[x] ) by A1; ::_thesis: ( S1[x] implies x in A )
set A =  {  aa where aa is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) )  }  ;
assume A4: S1[x] ; ::_thesis: x in A
then consider a being set  such that
A5: a in X . s and
A6: x = root-tree [a,s] ;
A7: (FreeSort X) . s = FreeSort (X,s) by Def11;
set sa = [a,s];
 [a,s] in coprod (s,X) by A5, Def2;
then  [a,s] in union (rng (coprod X)) by A2, TARSKI:def_4;
then A8: [a,s] in Terminals (DTConMSA X) by A3, CARD_3:def_4;
then reconsider sa = [a,s] as Symbol of (DTConMSA X) ;
reconsider b = root-tree sa as Element of TS (DTConMSA X) by A8, DTCONSTR:def_1;
 b in  {  aa where aa is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & aa = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = aa . {} & the_result_sort_of o1 = s ) )  }  by A5;
hence  x in A by A1, A4, A6, A7; ::_thesis: verum
end;
hence  ex b1 being Subset of ((FreeSort X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of ((FreeSort X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) holds
b1 = b2
proof
let A, B be Subset of ((FreeSort X) . s); ::_thesis: ( ( for x being set holds
( x in A iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being set holds
( x in B iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) implies A = B )
assume that
A9: for x being set holds
( x in A iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) and
A10: for x being set holds
( x in B iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ; ::_thesis: A = B
thus  A c= B :: according to XBOOLE_0:def_10 ::_thesis: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
then  ex a being set st
( a in X . s & x = root-tree [a,s] ) by A9;
hence  x in B by A10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume  x in B ; ::_thesis: x in A
then  ex a being set st
( a in X . s & x = root-tree [a,s] ) by A10;
hence  x in A by A9; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines FreeGen MSAFREE:def_15_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Subset of ((FreeSort X) . s) holds
( b4 = FreeGen (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) );

registration
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
cluster FreeGen (s,X) ->  non empty ;
coherence
 not FreeGen (s,X) is empty
proof
consider x being set  such that
A1: x in X . s by XBOOLE_0:def_1;
 ex a being set st
( a in X . s & root-tree [x,s] = root-tree [a,s] ) by A1;
hence  not FreeGen (s,X) is empty by Def15; ::_thesis: verum
end;
end;

theorem Th13: :: MSAFREE:13
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }
let X be V16() ManySortedSet of the carrier of S; ::_thesis: for s being SortSymbol of S holds FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }
let s be SortSymbol of S; ::_thesis: FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }
set D = DTConMSA X;
set A =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  ;
thus  FreeGen (s,X) c=  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  c= FreeGen (s,X)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FreeGen (s,X) or x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  )
assume  x in FreeGen (s,X) ; ::_thesis: x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }
then consider a being set  such that
A1: a in X . s and
A2: x = root-tree [a,s] by Def15;
A3: [a,s] in Terminals (DTConMSA X) by A1, Th7;
then reconsider t = [a,s] as Symbol of (DTConMSA X) ;
 t `2 = s by MCART_1:7;
hence  x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  by A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  or x in FreeGen (s,X) )
assume  x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  ; ::_thesis: x in FreeGen (s,X)
then consider t being Symbol of (DTConMSA X) such that
A4: x = root-tree t and
A5: t in Terminals (DTConMSA X) and
A6: t `2 = s ;
consider s1 being SortSymbol of S, a being set  such that
A7: a in X . s1 and
A8: t = [a,s1] by A5, Th7;
 s = s1 by A6, A8, MCART_1:7;
hence  x in FreeGen (s,X) by A4, A7, A8, Def15; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func FreeGen X ->  GeneratorSet of FreeMSA X means :Def16: :: MSAFREE:def 16
 for s being SortSymbol of S holds it . s = FreeGen (s,X);
existence
 ex b1 being GeneratorSet of FreeMSA X st
for s being SortSymbol of S holds b1 . s = FreeGen (s,X)
proof
deffunc H1( Element of S) ->  Subset of ((FreeSort X) . $1) = FreeGen ($1,X);
set FM = FreeMSA X;
set D = DTConMSA X;
consider f being Function such that
A1: ( dom f = the carrier of S & ( for s being Element of S holds f . s = H1(s) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S by A1, PARTFUN1:def_2, RELAT_1:def_18;
 f c= the Sorts of (FreeMSA X)
proof
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S or f . x c= the Sorts of (FreeMSA X) . x )
assume  x in the carrier of S ; ::_thesis: f . x c= the Sorts of (FreeMSA X) . x
then reconsider s = x as SortSymbol of S ;
 f . s = FreeGen (s,X) by A1;
hence  f . x c= the Sorts of (FreeMSA X) . x ; ::_thesis: verum
end;
then reconsider f = f as MSSubset of (FreeMSA X) by PBOOLE:def_18;
 the Sorts of (GenMSAlg f) = the Sorts of (FreeMSA X)
proof
defpred S1[ set ] means $1 in union (rng the Sorts of (GenMSAlg f));
 the Sorts of (GenMSAlg f) is MSSubset of (FreeMSA X) by MSUALG_2:def_9;
then A2: the Sorts of (GenMSAlg f) c= the Sorts of (FreeMSA X) by PBOOLE:def_18;
A3: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
set G = GenMSAlg f;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
let nt be Symbol of (DTConMSA X); ::_thesis: for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
let ts be FinSequence of TS (DTConMSA X); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ; ::_thesis: S1[nt -tree ts]
reconsider sy = nt as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
A6: [nt,(roots ts)] in the Rules of (DTConMSA X) by A4, LANG1:def_1;
then reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
 [sy,rt] in REL X by A4, LANG1:def_1;
then  sy in [: the carrier' of S,{ the carrier of S}:] by Def7;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A7: sy = [o,x2] by DOMAIN_1:1;
set ar = the_arity_of o;
set rs = the_result_sort_of o;
A8: x2 = the carrier of S by TARSKI:def_1;
 [nt,(roots ts)] in REL X by A4, LANG1:def_1;
then A9: len rt = len (the_arity_of o) by A7, A8, Th5;
reconsider B = the Sorts of (GenMSAlg f) as MSSubset of (FreeMSA X) by MSUALG_2:def_9;
A10: dom B = the carrier of S by PARTFUN1:def_2;
A11: dom (roots ts) = dom ts by TREES_3:def_18;
 rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then A12: dom (B * (the_arity_of o)) = dom (the_arity_of o) by A10, RELAT_1:27;
A13: ( Seg (len rt) = dom rt & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def_3;
then A14: dom ts = dom (the_arity_of o) by A6, A7, A8, A11, Th5;
A15: for x being set st x in dom (B * (the_arity_of o)) holds
ts . x in (B * (the_arity_of o)) . x
proof
let x be set ; ::_thesis: ( x in dom (B * (the_arity_of o)) implies ts . x in (B * (the_arity_of o)) . x )
assume A16: x in dom (B * (the_arity_of o)) ; ::_thesis: ts . x in (B * (the_arity_of o)) . x
then reconsider n = x as Nat ;
A17: ts . n in rng ts by A12, A11, A9, A13, A16, FUNCT_1:def_3;
 rng ts c= TS (DTConMSA X) by FINSEQ_1:def_4;
then reconsider T = ts . x as Element of TS (DTConMSA X) by A17;
 S1[T] by A5, A17;
then consider A being set  such that
A18: T in A and
A19: A in rng the Sorts of (GenMSAlg f) by TARSKI:def_4;
set b = (the_arity_of o) /. n;
set A1 =  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) )  }  ;
A20:  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) )  }  = FreeSort (X,((the_arity_of o) /. n))
.= (FreeSort X) . ((the_arity_of o) /. n) by Def11 ;
A21: ex t being DecoratedTree st
( t = ts . n & rt . n = t . {} ) by A12, A11, A9, A13, A16, TREES_3:def_18;
consider s being set  such that
A22: s in dom the Sorts of (GenMSAlg f) and
A23: the Sorts of (GenMSAlg f) . s = A by A19, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A22;
A24: ( rng rt c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & rt . n in rng rt ) by A12, A9, A13, A16, FINSEQ_1:def_4, FUNCT_1:def_3;
A25: now__::_thesis:_T_in_(FreeSort_X)_._((the_arity_of_o)_/._n)
percases ( rt . n in [: the carrier' of S,{ the carrier of S}:] or rt . n in Union (coprod X) ) by A24, XBOOLE_0:def_3;
supposeA26: rt . n in [: the carrier' of S,{ the carrier of S}:] ; ::_thesis: T in (FreeSort X) . ((the_arity_of o) /. n)
then consider o1 being OperSymbol of S, x2 being Element of { the carrier of S} such that
A27: rt . n = [o1,x2] by DOMAIN_1:1;
A28: x2 = the carrier of S by TARSKI:def_1;
then  the_result_sort_of o1 = (the_arity_of o) . n by A6, A7, A8, A12, A11, A14, A16, A26, A27, Th5
.= (the_arity_of o) /. n by A12, A16, PARTFUN1:def_6 ;
hence  T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A21, A27, A28; ::_thesis: verum
end;
supposeA29: rt . n in Union (coprod X) ; ::_thesis: T in (FreeSort X) . ((the_arity_of o) /. n)
then  rt . n in coprod (((the_arity_of o) . n),X) by A6, A7, A8, A12, A11, A14, A16, Th5;
then  rt . n in coprod (((the_arity_of o) /. n),X) by A12, A16, PARTFUN1:def_6;
then A30: ex a being set st
( a in X . ((the_arity_of o) /. n) & rt . n = [a,((the_arity_of o) /. n)] ) by Def2;
reconsider tt = rt . n as Terminal of (DTConMSA X) by A29, Th6;
 T = root-tree tt by A21, DTCONSTR:9;
hence  T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A30; ::_thesis: verum
end;
end;
end;
A31: now__::_thesis:_not_(the_arity_of_o)_/._n_<>_s
assume  (the_arity_of o) /. n <> s ; ::_thesis: contradiction
then A32: (FreeSort X) . s misses (FreeSort X) . ((the_arity_of o) /. n) by Th12;
 the Sorts of (GenMSAlg f) . s c= the Sorts of (FreeMSA X) . s by A2, PBOOLE:def_2;
hence  contradiction by A18, A23, A25, A32, XBOOLE_0:3; ::_thesis: verum
end;
(B * (the_arity_of o)) . x = B . ((the_arity_of o) . n) by A16, FUNCT_1:12
.= B . ((the_arity_of o) /. n) by A12, A16, PARTFUN1:def_6 ;
hence  ts . x in (B * (the_arity_of o)) . x by A18, A23, A31; ::_thesis: verum
end;
set AR = the Arity of S;
set RS = the ResultSort of S;
set BH = (B #) * the Arity of S;
set O = the carrier' of S;
A33: Den (o,(FreeMSA X)) = (FreeOper X) . o by MSUALG_1:def_6
.= DenOp (o,X) by Def13 ;
A34: ( Sym (o,X) = [o, the carrier of S] & nt = [o, the carrier of S] ) by A7, TARSKI:def_1;
 the Arity of S . o = the_arity_of o by MSUALG_1:def_1;
then  ((B #) * the Arity of S) . o = product (B * (the_arity_of o)) by Th1;
then A35: ts in ((B #) * the Arity of S) . o by A12, A11, A9, A13, A15, CARD_3:9;
 dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o by FUNCT_2:def_1;
then  ts in dom (DenOp (o,X)) by A4, A34, Th10;
then  ts in (dom (DenOp (o,X))) /\ (((B #) * the Arity of S) . o) by A35, XBOOLE_0:def_4;
then A36: ts in dom ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) by RELAT_1:61;
then ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) . ts = (DenOp (o,X)) . ts by FUNCT_1:47
.= nt -tree ts by A4, A34, Def12 ;
then A37: nt -tree ts in rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) by A33, A36, FUNCT_1:def_3;
 ( the ResultSort of S . o = the_result_sort_of o & dom (B * the ResultSort of S) = the carrier' of S ) by MSUALG_1:def_2, PARTFUN1:def_2;
then A38: (B * the ResultSort of S) . o = B . (the_result_sort_of o) by FUNCT_1:12;
 B is opers_closed by MSUALG_2:def_9;
then  B is_closed_on o by MSUALG_2:def_6;
then A39: rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by MSUALG_2:def_5;
 B . (the_result_sort_of o) in rng B by A10, FUNCT_1:def_3;
hence  S1[nt -tree ts] by A39, A37, A38, TARSKI:def_4; ::_thesis: verum
end;
A40: for s being Symbol of (DTConMSA X) st s in Terminals (DTConMSA X) holds
S1[ root-tree s]
proof
let t be Symbol of (DTConMSA X); ::_thesis: ( t in Terminals (DTConMSA X) implies S1[ root-tree t] )
assume  t in Terminals (DTConMSA X) ; ::_thesis: S1[ root-tree t]
then  t in Union (coprod X) by Th6;
then  t in union (rng (coprod X)) by CARD_3:def_4;
then consider A being set  such that
A41: t in A and
A42: A in rng (coprod X) by TARSKI:def_4;
consider s being set  such that
A43: s in dom (coprod X) and
A44: (coprod X) . s = A by A42, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A43;
 A = coprod (s,X) by A44, Def3;
then  ex a being set st
( a in X . s & t = [a,s] ) by A41, Def2;
then A45: root-tree t in FreeGen (s,X) by Def15;
 f is MSSubset of (GenMSAlg f) by MSUALG_2:def_17;
then  f c= the Sorts of (GenMSAlg f) by PBOOLE:def_18;
then  f . s c= the Sorts of (GenMSAlg f) . s by PBOOLE:def_2;
then A46: FreeGen (s,X) c= the Sorts of (GenMSAlg f) . s by A1;
 dom the Sorts of (GenMSAlg f) = the carrier of S by PARTFUN1:def_2;
then  the Sorts of (GenMSAlg f) . s in rng the Sorts of (GenMSAlg f) by FUNCT_1:def_3;
hence  S1[ root-tree t] by A46, A45, TARSKI:def_4; ::_thesis: verum
end;
A47: for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S1[t] from DTCONSTR:sch_7(A40, A3);
A48: union (rng the Sorts of (FreeMSA X)) c= union (rng the Sorts of (GenMSAlg f))
proof
set D = DTConMSA X;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng the Sorts of (FreeMSA X)) or x in union (rng the Sorts of (GenMSAlg f)) )
assume  x in union (rng the Sorts of (FreeMSA X)) ; ::_thesis: x in union (rng the Sorts of (GenMSAlg f))
then consider A being set  such that
A49: x in A and
A50: A in rng the Sorts of (FreeMSA X) by TARSKI:def_4;
consider s being set  such that
A51: s in dom (FreeSort X) and
A52: (FreeSort X) . s = A by A50, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A51;
A = FreeSort (X,s) by A52, Def11
.=  {  a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) )  }  ;
then  ex a being Element of TS (DTConMSA X) st
( a = x & ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st
( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A49;
hence  x in union (rng the Sorts of (GenMSAlg f)) by A47; ::_thesis: verum
end;
let x be Element of S; :: according to PBOOLE:def_21 ::_thesis: the Sorts of (GenMSAlg f) . x = the Sorts of (FreeMSA X) . x
reconsider s = x as SortSymbol of S ;
thus  the Sorts of (GenMSAlg f) . x c= the Sorts of (FreeMSA X) . x by A2, PBOOLE:def_2; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the Sorts of (FreeMSA X) . x or a in the Sorts of (GenMSAlg f) . x )
assume A53: a in the Sorts of (FreeMSA X) . x ; ::_thesis: a in the Sorts of (GenMSAlg f) . x
 the carrier of S = dom the Sorts of (FreeMSA X) by PARTFUN1:def_2;
then  the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def_3;
then  a in union (rng the Sorts of (FreeMSA X)) by A53, TARSKI:def_4;
then consider A being set  such that
A54: a in A and
A55: A in rng the Sorts of (GenMSAlg f) by A48, TARSKI:def_4;
consider b being set  such that
A56: b in dom the Sorts of (GenMSAlg f) and
A57: the Sorts of (GenMSAlg f) . b = A by A55, FUNCT_1:def_3;
reconsider b = b as SortSymbol of S by A56;
now__::_thesis:_not_b_<>_s
assume  b <> s ; ::_thesis: contradiction
then  (FreeSort X) . s misses (FreeSort X) . b by Th12;
then A58: ((FreeSort X) . s) /\ ((FreeSort X) . b) = {} by XBOOLE_0:def_7;
 the Sorts of (GenMSAlg f) . b c= the Sorts of (FreeMSA X) . b by A2, PBOOLE:def_2;
hence  contradiction by A53, A54, A57, A58, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a in the Sorts of (GenMSAlg f) . x by A54, A57; ::_thesis: verum
end;
then reconsider f = f as GeneratorSet of FreeMSA X by Def4;
take  f ; ::_thesis: for s being SortSymbol of S holds f . s = FreeGen (s,X)
thus  for s being SortSymbol of S holds f . s = FreeGen (s,X) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being GeneratorSet of FreeMSA X st ( for s being SortSymbol of S holds b1 . s = FreeGen (s,X) ) & ( for s being SortSymbol of S holds b2 . s = FreeGen (s,X) ) holds
b1 = b2
proof
let A, B be GeneratorSet of FreeMSA X; ::_thesis: ( ( for s being SortSymbol of S holds A . s = FreeGen (s,X) ) & ( for s being SortSymbol of S holds B . s = FreeGen (s,X) ) implies A = B )
assume that
A59: for s being SortSymbol of S holds A . s = FreeGen (s,X) and
A60: for s being SortSymbol of S holds B . s = FreeGen (s,X) ; ::_thesis: A = B
 for i being set st i in the carrier of S holds
A . i = B . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies A . i = B . i )
assume  i in the carrier of S ; ::_thesis: A . i = B . i
then reconsider s = i as SortSymbol of S ;
 A . s = FreeGen (s,X) by A59;
hence  A . i = B . i by A60; ::_thesis: verum
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines FreeGen MSAFREE:def_16_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being GeneratorSet of FreeMSA X holds
( b3 = FreeGen X iff for s being SortSymbol of S holds b3 . s = FreeGen (s,X) );

theorem :: MSAFREE:14
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()
let X be V16() ManySortedSet of the carrier of S; ::_thesis: FreeGen X is V16()
let x be set ; :: according to PBOOLE:def_13 ::_thesis: ( not x in the carrier of S or not (FreeGen X) . x is empty )
assume  x in the carrier of S ; ::_thesis: not (FreeGen X) . x is empty
then reconsider s = x as SortSymbol of S ;
 (FreeGen X) . s = FreeGen (s,X) by Def16;
hence  not (FreeGen X) . x is empty ; ::_thesis: verum
end;

theorem :: MSAFREE:15
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }
let X be V16() ManySortedSet of the carrier of S; ::_thesis: union (rng (FreeGen X)) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }
set D = DTConMSA X;
set A = union (rng (FreeGen X));
set B =  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  ;
thus  union (rng (FreeGen X)) c=  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  c= union (rng (FreeGen X))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng (FreeGen X)) or x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  )
assume  x in union (rng (FreeGen X)) ; ::_thesis: x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }
then consider C being set  such that
A1: x in C and
A2: C in rng (FreeGen X) by TARSKI:def_4;
consider s being set  such that
A3: s in dom (FreeGen X) and
A4: (FreeGen X) . s = C by A2, FUNCT_1:def_3;
reconsider s = s as SortSymbol of S by A3;
C = FreeGen (s,X) by A4, Def16
.=  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  by Th13 ;
then  ex t being Symbol of (DTConMSA X) st
( x = root-tree t & t in Terminals (DTConMSA X) & t `2 = s ) by A1;
hence  x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  or x in union (rng (FreeGen X)) )
assume  x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X)  }  ; ::_thesis: x in union (rng (FreeGen X))
then consider t being Symbol of (DTConMSA X) such that
A5: x = root-tree t and
A6: t in Terminals (DTConMSA X) ;
consider s being SortSymbol of S, a being set  such that
 a in X . s and
A7: t = [a,s] by A6, Th7;
 t `2 = s by A7, MCART_1:7;
then  x in  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  by A5, A6;
then  x in FreeGen (s,X) by Th13;
then A8: x in (FreeGen X) . s by Def16;
 dom (FreeGen X) = the carrier of S by PARTFUN1:def_2;
then  (FreeGen X) . s in rng (FreeGen X) by FUNCT_1:def_3;
hence  x in union (rng (FreeGen X)) by A8, TARSKI:def_4; ::_thesis: verum
end;

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
func Reverse (s,X) ->  Function of (FreeGen (s,X)),(X . s) means :Def17: :: MSAFREE:def 17
 for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
it . (root-tree t) = t `1 ;
existence
 ex b1 being Function of (FreeGen (s,X)),(X . s) st
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1
proof
set A = FreeGen (s,X);
set D = DTConMSA X;
defpred S1[ set , set ] means  for t being Symbol of (DTConMSA X) st $1 = root-tree t holds
$2 = t `1 ;
A1: for x being set st x in FreeGen (s,X) holds
ex a being set st
( a in X . s & S1[x,a] )
proof
let x be set ; ::_thesis: ( x in FreeGen (s,X) implies ex a being set st
( a in X . s & S1[x,a] ) )
assume  x in FreeGen (s,X) ; ::_thesis: ex a being set st
( a in X . s & S1[x,a] )
then  x in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  by Th13;
then consider t being Symbol of (DTConMSA X) such that
A2: x = root-tree t and
A3: t in Terminals (DTConMSA X) and
A4: t `2 = s ;
consider s1 being SortSymbol of S, a being set  such that
A5: a in X . s1 and
A6: t = [a,s1] by A3, Th7;
take  a ; ::_thesis: ( a in X . s & S1[x,a] )
thus  a in X . s by A4, A5, A6, MCART_1:7; ::_thesis: S1[x,a]
let t1 be Symbol of (DTConMSA X); ::_thesis: ( x = root-tree t1 implies a = t1 `1 )
assume  x = root-tree t1 ; ::_thesis: a = t1 `1
then  t = t1 by A2, TREES_4:4;
hence  a = t1 `1 by A6, MCART_1:7; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = FreeGen (s,X) & rng f c= X . s & ( for x being set st x in FreeGen (s,X) holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A1);
reconsider f = f as Function of (FreeGen (s,X)),(X . s) by A7, FUNCT_2:2;
take  f ; ::_thesis: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
f . (root-tree t) = t `1
let t be Symbol of (DTConMSA X); ::_thesis: ( root-tree t in FreeGen (s,X) implies f . (root-tree t) = t `1 )
assume  root-tree t in FreeGen (s,X) ; ::_thesis: f . (root-tree t) = t `1
hence  f . (root-tree t) = t `1 by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (FreeGen (s,X)),(X . s) st ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b1 . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b2 . (root-tree t) = t `1 ) holds
b1 = b2
proof
set D = DTConMSA X;
set C =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  ;
let A, B be Function of (FreeGen (s,X)),(X . s); ::_thesis: ( ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
A . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
B . (root-tree t) = t `1 ) implies A = B )
assume that
A8: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
A . (root-tree t) = t `1 and
A9: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
B . (root-tree t) = t `1 ; ::_thesis: A = B
A10: FreeGen (s,X) =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  by Th13;
A11: for i being set st i in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  holds
A . i = B . i
proof
let i be set ; ::_thesis: ( i in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  implies A . i = B . i )
assume A12: i in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  ; ::_thesis: A . i = B . i
then consider t being Symbol of (DTConMSA X) such that
A13: i = root-tree t and
 t in Terminals (DTConMSA X) and
 t `2 = s ;
 A . (root-tree t) = t `1 by A8, A10, A12, A13;
hence  A . i = B . i by A9, A10, A12, A13; ::_thesis: verum
end;
 ( dom A =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  & dom B =  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  ) by A10, FUNCT_2:def_1;
hence  A = B by A11, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def17 defines Reverse MSAFREE:def_17_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b4 being Function of (FreeGen (s,X)),(X . s) holds
( b4 = Reverse (s,X) iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b4 . (root-tree t) = t `1 );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
func Reverse X ->  ManySortedFunction of FreeGen X,X means :Def18: :: MSAFREE:def 18
 for s being SortSymbol of S holds it . s = Reverse (s,X);
existence
 ex b1 being ManySortedFunction of FreeGen X,X st
for s being SortSymbol of S holds b1 . s = Reverse (s,X)
proof
defpred S1[ set , set ] means  for s being SortSymbol of S st s = $1 holds
$2 = Reverse (s,X);
set I = the carrier of S;
set FG = FreeGen X;
A1: for i being set st i in the carrier of S holds
ex u being set st S1[i,u]
proof
let i be set ; ::_thesis: ( i in the carrier of S implies ex u being set st S1[i,u] )
assume  i in the carrier of S ; ::_thesis: ex u being set st S1[i,u]
then reconsider s = i as SortSymbol of S ;
take  Reverse (s,X) ; ::_thesis: S1[i, Reverse (s,X)]
let s1 be SortSymbol of S; ::_thesis: ( s1 = i implies Reverse (s,X) = Reverse (s1,X) )
assume  s1 = i ; ::_thesis: Reverse (s,X) = Reverse (s1,X)
hence  Reverse (s,X) = Reverse (s1,X) ; ::_thesis: verum
end;
consider H being Function such that
A2: ( dom H = the carrier of S & ( for i being set st i in the carrier of S holds
S1[i,H . i] ) ) from CLASSES1:sch_1(A1);
reconsider H = H as ManySortedSet of the carrier of S by A2, PARTFUN1:def_2, RELAT_1:def_18;
 for x being set st x in dom H holds
H . x is Function
proof
let i be set ; ::_thesis: ( i in dom H implies H . i is Function )
assume  i in dom H ; ::_thesis: H . i is Function
then reconsider s = i as SortSymbol of S ;
 H . s = Reverse (s,X) by A2;
hence  H . i is Function ; ::_thesis: verum
end;
then reconsider H = H as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
 for i being set st i in the carrier of S holds
H . i is Function of ((FreeGen X) . i),(X . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies H . i is Function of ((FreeGen X) . i),(X . i) )
assume  i in the carrier of S ; ::_thesis: H . i is Function of ((FreeGen X) . i),(X . i)
then reconsider s = i as SortSymbol of S ;
 ( (FreeGen X) . s = FreeGen (s,X) & H . i = Reverse (s,X) ) by A2, Def16;
hence  H . i is Function of ((FreeGen X) . i),(X . i) ; ::_thesis: verum
end;
then reconsider H = H as ManySortedFunction of FreeGen X,X by PBOOLE:def_15;
take  H ; ::_thesis: for s being SortSymbol of S holds H . s = Reverse (s,X)
let s be SortSymbol of S; ::_thesis: H . s = Reverse (s,X)
thus  H . s = Reverse (s,X) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being ManySortedFunction of FreeGen X,X st ( for s being SortSymbol of S holds b1 . s = Reverse (s,X) ) & ( for s being SortSymbol of S holds b2 . s = Reverse (s,X) ) holds
b1 = b2
proof
let A, B be ManySortedFunction of FreeGen X,X; ::_thesis: ( ( for s being SortSymbol of S holds A . s = Reverse (s,X) ) & ( for s being SortSymbol of S holds B . s = Reverse (s,X) ) implies A = B )
assume that
A3: for s being SortSymbol of S holds A . s = Reverse (s,X) and
A4: for s being SortSymbol of S holds B . s = Reverse (s,X) ; ::_thesis: A = B
 for i being set st i in the carrier of S holds
A . i = B . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies A . i = B . i )
assume  i in the carrier of S ; ::_thesis: A . i = B . i
then reconsider s = i as SortSymbol of S ;
 A . s = Reverse (s,X) by A3;
hence  A . i = B . i by A4; ::_thesis: verum
end;
hence  A = B by PBOOLE:3; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines Reverse MSAFREE:def_18_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for b3 being ManySortedFunction of FreeGen X,X holds
( b3 = Reverse X iff for s being SortSymbol of S holds b3 . s = Reverse (s,X) );

definition
let S be non empty non void ManySortedSign ;
let X, A be V16() ManySortedSet of the carrier of S;
let F be ManySortedFunction of FreeGen X,A;
let t be Symbol of (DTConMSA X);
assume A1: t in Terminals (DTConMSA X) ;
func pi (F,A,t) ->  Element of Union A means :Def19: :: MSAFREE:def 19
 for f being Function st f = F . (t `2) holds
it = f . (root-tree t);
existence
 ex b1 being Element of Union A st
for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t)
proof
set FG = FreeGen X;
set D = DTConMSA X;
consider s being SortSymbol of S, x being set  such that
 x in X . s and
A2: t = [x,s] by A1, Th7;
 (FreeGen X) . s = FreeGen (s,X) by Def16;
then A3: dom (F . s) = FreeGen (s,X) by FUNCT_2:def_1
.=  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  by Th13 ;
 t `2 = s by A2, MCART_1:7;
then  root-tree t in dom (F . s) by A1, A3;
then A4: (F . s) . (root-tree t) in rng (F . s) by FUNCT_1:def_3;
 dom A = the carrier of S by PARTFUN1:def_2;
then  ( rng (F . s) c= A . s & A . s in rng A ) by FUNCT_1:def_3, RELAT_1:def_19;
then  (F . s) . (root-tree t) in union (rng A) by A4, TARSKI:def_4;
then reconsider eu = (F . s) . (root-tree t) as Element of Union A by CARD_3:def_4;
take  eu ; ::_thesis: for f being Function st f = F . (t `2) holds
eu = f . (root-tree t)
let f be Function; ::_thesis: ( f = F . (t `2) implies eu = f . (root-tree t) )
assume  f = F . (t `2) ; ::_thesis: eu = f . (root-tree t)
hence  eu = f . (root-tree t) by A2, MCART_1:7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of Union A st ( for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t) ) & ( for f being Function st f = F . (t `2) holds
b2 = f . (root-tree t) ) holds
b1 = b2
proof
consider s being SortSymbol of S, x being set  such that
 x in X . s and
A5: t = [x,s] by A1, Th7;
reconsider f = F . s as Function ;
let a, b be Element of Union A; ::_thesis: ( ( for f being Function st f = F . (t `2) holds
a = f . (root-tree t) ) & ( for f being Function st f = F . (t `2) holds
b = f . (root-tree t) ) implies a = b )
assume that
A6: for f being Function st f = F . (t `2) holds
a = f . (root-tree t) and
A7: for f being Function st f = F . (t `2) holds
b = f . (root-tree t) ; ::_thesis: a = b
A8: f = F . (t `2) by A5, MCART_1:7;
then  a = f . (root-tree t) by A6;
hence  a = b by A7, A8; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines pi MSAFREE:def_19_:_
 for S being non empty non void ManySortedSign
for X, A being V16() ManySortedSet of the carrier of S
for F being ManySortedFunction of FreeGen X,A
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
for b6 being Element of Union A holds
( b6 = pi (F,A,t) iff for f being Function st f = F . (t `2) holds
b6 = f . (root-tree t) );

definition
let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let t be Symbol of (DTConMSA X);
assume A1: ex p being FinSequence st t ==> p ;
func @ (X,t) ->  OperSymbol of S means :Def20: :: MSAFREE:def 20
[it, the carrier of S] = t;
existence
 ex b1 being OperSymbol of S st [b1, the carrier of S] = t
proof
set D = DTConMSA X;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
reconsider a = t as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;
consider p being FinSequence such that
A2: t ==> p by A1;
 [t,p] in the Rules of (DTConMSA X) by A2, LANG1:def_1;
then reconsider p = p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
 [a,p] in REL X by A2, LANG1:def_1;
then  a in [: the carrier' of S,{ the carrier of S}:] by Def7;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A3: a = [o,x2] by DOMAIN_1:1;
take  o ; ::_thesis: [o, the carrier of S] = t
thus  [o, the carrier of S] = t by A3, TARSKI:def_1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being OperSymbol of S st [b1, the carrier of S] = t & [b2, the carrier of S] = t holds
b1 = b2 by XTUPLE_0:1;
end;

:: deftheorem Def20 defines @ MSAFREE:def_20_:_
 for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for t being Symbol of (DTConMSA X) st ex p being FinSequence st t ==> p holds
for b4 being OperSymbol of S holds
( b4 = @ (X,t) iff [b4, the carrier of S] = t );

definition
let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let p be FinSequence;
assume A1: p in Args (o,U0) ;
func pi (o,U0,p) ->  Element of Union the Sorts of U0 equals :Def21: :: MSAFREE:def 21
(Den (o,U0)) . p;
coherence
 (Den (o,U0)) . p is Element of Union the Sorts of U0
proof
set F = Den (o,U0);
set S0 = the Sorts of U0;
 dom (Den (o,U0)) = Args (o,U0) by FUNCT_2:def_1;
then  ( rng (Den (o,U0)) c= Result (o,U0) & (Den (o,U0)) . p in rng (Den (o,U0)) ) by A1, FUNCT_1:def_3, RELAT_1:def_19;
then  (Den (o,U0)) . p in union (rng the Sorts of U0) by TARSKI:def_4;
hence  (Den (o,U0)) . p is Element of Union the Sorts of U0 by CARD_3:def_4; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines pi MSAFREE:def_21_:_
 for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,U0) holds
pi (o,U0,p) = (Den (o,U0)) . p;

theorem Th16: :: MSAFREE:16
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free
let X be V16() ManySortedSet of the carrier of S; ::_thesis: FreeGen X is free
set D = DTConMSA X;
set FA = FreeMSA X;
set FG = FreeGen X;
let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def_5 ::_thesis: for f being ManySortedFunction of FreeGen X, the Sorts of U1 ex h being ManySortedFunction of (FreeMSA X),U1 st
( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = f )
let F be ManySortedFunction of FreeGen X, the Sorts of U1; ::_thesis: ex h being ManySortedFunction of (FreeMSA X),U1 st
( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )
set SA = the Sorts of (FreeMSA X);
set AR = the Arity of S;
set S1 = the Sorts of U1;
set O = the carrier' of S;
set RS = the ResultSort of S;
set DU = Union the Sorts of U1;
deffunc H1( Symbol of (DTConMSA X)) ->  Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);
deffunc H2( Symbol of (DTConMSA X), FinSequence, FinSequence) ->  Element of Union the Sorts of U1 = pi ((@ (X,$1)),U1,$3);
consider G being Function of (TS (DTConMSA X)),(Union the Sorts of U1) such that
A1: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
G . (root-tree t) = H1(t) and
A2: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts holds
G . (nt -tree ts) = H2(nt, roots ts,G * ts) from DTCONSTR:sch_8();
deffunc H3( set ) ->  Element of bool [:(TS (DTConMSA X)),(Union the Sorts of U1):] = G | ( the Sorts of (FreeMSA X) . $1);
consider h being Function such that
A3: ( dom h = the carrier of S & ( for s being set st s in the carrier of S holds
h . s = H3(s) ) ) from FUNCT_1:sch_3();
reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def_2, RELAT_1:def_18;
 for s being set st s in dom h holds
h . s is Function
proof
let s be set ; ::_thesis: ( s in dom h implies h . s is Function )
assume  s in dom h ; ::_thesis: h . s is Function
then  h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
hence  h . s is Function ; ::_thesis: verum
end;
then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def_6;
defpred S1[ set ] means  for s being SortSymbol of S st $1 in the Sorts of (FreeMSA X) . s holds
(h . s) . $1 in the Sorts of U1 . s;
A4: for nt being Symbol of (DTConMSA X)
for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
let nt be Symbol of (DTConMSA X); ::_thesis: for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
let ts be FinSequence of TS (DTConMSA X); ::_thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds
S1[t] ; ::_thesis: S1[nt -tree ts]
set p = G * ts;
set o = @ (X,nt);
set ar = the_arity_of (@ (X,nt));
set rs = the_result_sort_of (@ (X,nt));
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set rt = roots ts;
A7: [(@ (X,nt)), the carrier of S] = nt by A5, Def20;
then A8: [[(@ (X,nt)), the carrier of S],(roots ts)] in the Rules of (DTConMSA X) by A5, LANG1:def_1;
A9: [(@ (X,nt)), the carrier of S] = Sym ((@ (X,nt)),X) ;
then A10: (DenOp ((@ (X,nt)),X)) . ts = nt -tree ts by A5, A7, Def12;
 dom (DenOp ((@ (X,nt)),X)) = (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by FUNCT_2:def_1;
then  ts in dom (DenOp ((@ (X,nt)),X)) by A5, A7, A9, Th10;
then  ( rng (DenOp ((@ (X,nt)),X)) c= ((FreeSort X) * the ResultSort of S) . (@ (X,nt)) & nt -tree ts in rng (DenOp ((@ (X,nt)),X)) ) by A10, FUNCT_1:def_3, RELAT_1:def_19;
then A11: nt -tree ts in ( the Sorts of (FreeMSA X) * the ResultSort of S) . (@ (X,nt)) ;
set ppi = pi ((@ (X,nt)),U1,(G * ts));
A12: rng the ResultSort of S c= the carrier of S by RELAT_1:def_19;
A13: rng (the_arity_of (@ (X,nt))) c= the carrier of S by FINSEQ_1:def_4;
reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, ZFMISC_1:87;
A14: len rt = len (the_arity_of (@ (X,nt))) by A8, Th5;
A15: dom rt = Seg (len rt) by FINSEQ_1:def_3;
 dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def_2;
then A16: dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;
A17: the_arity_of (@ (X,nt)) = the Arity of S . (@ (X,nt)) by MSUALG_1:def_1;
 dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A18: dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;
A19: ( dom rt = dom ts & Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) ) by FINSEQ_1:def_3, TREES_3:def_18;
A20: dom (G * ts) = dom ts by FINSEQ_3:120;
then A21: dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A18, A8, A15, A19, Th5;
A22: for x being set st x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
proof
let x be set ; ::_thesis: ( x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) implies (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x )
assume A23: x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) ; ::_thesis: (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
then reconsider n = x as Nat ;
A24: ts . n in rng ts by A18, A14, A15, A19, A23, FUNCT_1:def_3;
 rng ts c= TS (DTConMSA X) by FINSEQ_1:def_4;
then reconsider t = ts . n as Element of TS (DTConMSA X) by A24;
A25: (G * ts) . n = G . (ts . n) by A21, A23, FINSEQ_3:120;
 (the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt))) by A18, A23, FUNCT_1:def_3;
then reconsider s = (the_arity_of (@ (X,nt))) . x as SortSymbol of S by A13;
A26: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
 dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def_2;
then A27: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def_3;
dom G = TS (DTConMSA X) by FUNCT_2:def_1
.= union (rng the Sorts of (FreeMSA X)) by Th11 ;
then A28: dom (h . s) = the Sorts of (FreeMSA X) . s by A26, A27, RELAT_1:62, ZFMISC_1:74;
 ts in (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by A5, A7, A9, Th10;
then  ts in product ((FreeSort X) * (the_arity_of (@ (X,nt)))) by A17, Th1;
then  ts . x in ((FreeSort X) * (the_arity_of (@ (X,nt)))) . x by A18, A16, A23, CARD_3:9;
then A29: ts . x in (FreeSort X) . ((the_arity_of (@ (X,nt))) . x) by A18, A16, A23, FUNCT_1:12;
then  (h . s) . t in the Sorts of U1 . s by A6, A24;
then  G . t in the Sorts of U1 . s by A29, A26, A28, FUNCT_1:47;
hence  (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x by A23, A25, FUNCT_1:12; ::_thesis: verum
end;
 dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A30: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;
let s be SortSymbol of S; ::_thesis: ( nt -tree ts in the Sorts of (FreeMSA X) . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )
A31: dom (Den ((@ (X,nt)),U1)) = Args ((@ (X,nt)),U1) by FUNCT_2:def_1;
A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
 dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def_2;
then  dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;
then  nt -tree ts in the Sorts of (FreeMSA X) . ( the ResultSort of S . (@ (X,nt))) by A32, A11, FUNCT_1:12;
then A33: nt -tree ts in the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def_2;
Args ((@ (X,nt)),U1) = (( the Sorts of U1 #) * the Arity of S) . (@ (X,nt)) by MSUALG_1:def_4
.= product ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A17, Th1 ;
then A34: G * ts in Args ((@ (X,nt)),U1) by A20, A18, A14, A15, A19, A22, CARD_3:9;
then  pi ((@ (X,nt)),U1,(G * ts)) = (Den ((@ (X,nt)),U1)) . (G * ts) by Def21;
then  ( rng (Den ((@ (X,nt)),U1)) c= Result ((@ (X,nt)),U1) & pi ((@ (X,nt)),U1,(G * ts)) in rng (Den ((@ (X,nt)),U1)) ) by A34, A31, FUNCT_1:def_3, RELAT_1:def_19;
then A35: pi ((@ (X,nt)),U1,(G * ts)) in Result ((@ (X,nt)),U1) ;
assume A36: nt -tree ts in the Sorts of (FreeMSA X) . s ; ::_thesis: (h . s) . (nt -tree ts) in the Sorts of U1 . s
A37: now__::_thesis:_not_the_result_sort_of_(@_(X,nt))_<>_s
assume A38: the_result_sort_of (@ (X,nt)) <> s ; ::_thesis: contradiction
 (FreeSort X) . (the_result_sort_of (@ (X,nt))) meets (FreeSort X) . s by A33, A36, XBOOLE_0:3;
hence  contradiction by A38, Th12; ::_thesis: verum
end;
 G . (nt -tree ts) = pi ((@ (X,nt)),U1,(G * ts)) by A2, A5;
then A39: pi ((@ (X,nt)),U1,(G * ts)) = (G | ( the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts) by A33, FUNCT_1:49;
Result ((@ (X,nt)),U1) = ( the Sorts of U1 * the ResultSort of S) . (@ (X,nt)) by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . (@ (X,nt))) by A30, A32, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def_2 ;
hence  (h . s) . (nt -tree ts) in the Sorts of U1 . s by A3, A35, A39, A37; ::_thesis: verum
end;
A40: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
S1[ root-tree t]
proof
let t be Symbol of (DTConMSA X); ::_thesis: ( t in Terminals (DTConMSA X) implies S1[ root-tree t] )
assume A41: t in Terminals (DTConMSA X) ; ::_thesis: S1[ root-tree t]
then consider s being SortSymbol of S, x being set  such that
 x in X . s and
A42: t = [x,s] by Th7;
set E =  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  ;
set a = root-tree t;
A43: t `2 = s by A42, MCART_1:7;
then A44: root-tree t in  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  by A41;
let s1 be SortSymbol of S; ::_thesis: ( root-tree t in the Sorts of (FreeMSA X) . s1 implies (h . s1) . (root-tree t) in the Sorts of U1 . s1 )
reconsider f = F . s as Function of ((FreeGen X) . s),( the Sorts of U1 . s) ;
A45: dom f = (FreeGen X) . s by FUNCT_2:def_1;
A46:  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  = FreeGen (s,X) by Th13;
then  (FreeGen X) . s =  {  (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s )  }  by Def16;
then A47: ( rng f c= the Sorts of U1 . s & f . (root-tree t) in rng f ) by A44, A45, FUNCT_1:def_3, RELAT_1:def_19;
assume A48: root-tree t in the Sorts of (FreeMSA X) . s1 ; ::_thesis: (h . s1) . (root-tree t) in the Sorts of U1 . s1
A49: now__::_thesis:_not_s_<>_s1
 root-tree t in ((FreeSort X) . s) /\ ((FreeSort X) . s1) by A44, A46, A48, XBOOLE_0:def_4;
then A50: (FreeSort X) . s meets (FreeSort X) . s1 by XBOOLE_0:4;
assume  s <> s1 ; ::_thesis: contradiction
hence  contradiction by A50, Th12; ::_thesis: verum
end;
 h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
then (h . s) . (root-tree t) = G . (root-tree t) by A44, A46, FUNCT_1:49
.= pi (F, the Sorts of U1,t) by A1, A41
.= f . (root-tree t) by A41, A43, Def19 ;
hence  (h . s1) . (root-tree t) in the Sorts of U1 . s1 by A47, A49; ::_thesis: verum
end;
A51: for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
S1[t] from DTCONSTR:sch_7(A40, A4);
 for s being set st s in the carrier of S holds
h . s is Function of ( the Sorts of (FreeMSA X) . s),( the Sorts of U1 . s)
proof
let x be set ; ::_thesis: ( x in the carrier of S implies h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x) )
assume  x in the carrier of S ; ::_thesis: h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x)
then reconsider s = x as SortSymbol of S ;
A52: dom G = TS (DTConMSA X) by FUNCT_2:def_1
.= union (rng the Sorts of (FreeMSA X)) by Th11 ;
 dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def_2;
then A53: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def_3;
A54: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
then A55: dom (h . s) = the Sorts of (FreeMSA X) . s by A52, A53, RELAT_1:62, ZFMISC_1:74;
A56: the Sorts of (FreeMSA X) . s c= dom G by A52, A53, ZFMISC_1:74;
 rng (h . s) c= the Sorts of U1 . s
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng (h . s) or a in the Sorts of U1 . s )
assume  a in rng (h . s) ; ::_thesis: a in the Sorts of U1 . s
then consider T being set  such that
A57: T in dom (h . s) and
A58: (h . s) . T = a by FUNCT_1:def_3;
reconsider T = T as Element of TS (DTConMSA X) by A56, A55, A57, FUNCT_2:def_1;
 T in the Sorts of (FreeMSA X) . s by A54, A52, A53, A57, RELAT_1:62, ZFMISC_1:74;
hence  a in the Sorts of U1 . s by A51, A58; ::_thesis: verum
end;
hence  h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x) by A55, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
then reconsider h = h as ManySortedFunction of (FreeMSA X),U1 by PBOOLE:def_15;
take  h ; ::_thesis: ( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )
thus  h is_homomorphism FreeMSA X,U1 ::_thesis: h || (FreeGen X) = F
proof
 ( rng the ResultSort of S c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S ) by PARTFUN1:def_2, RELAT_1:def_19;
then A59: ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def_1, RELAT_1:27;
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(FreeMSA X)) = {} or for b1 being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b1) = (Den (o,U1)) . (h # b1) )
assume  Args (o,(FreeMSA X)) <> {} ; ::_thesis: for b1 being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b1) = (Den (o,U1)) . (h # b1)
let x be Element of Args (o,(FreeMSA X)); ::_thesis: (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = (Den (o,U1)) . (h # x)
set rs = the_result_sort_of o;
set DA = Den (o,(FreeMSA X));
set D1 = Den (o,U1);
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set ar = the_arity_of o;
A60: the_arity_of o = the Arity of S . o by MSUALG_1:def_1;
A61: Args (o,(FreeMSA X)) = (((FreeSort X) #) * the Arity of S) . o by MSUALG_1:def_4;
then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;
A62: Sym (o,X) ==> roots p by A61, Th10;
then A63: @ (X,(Sym (o,X))) = o by Def20;
A64: dom (G * p) = dom p by FINSEQ_3:120;
A65: x in (((FreeSort X) #) * the Arity of S) . o by A61;
A66: for a being set st a in dom p holds
(G * p) . a = (h # x) . a
proof
 ( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S ) by FINSEQ_1:def_4, PARTFUN1:def_2;
then A67: dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
set rt = roots p;
let a be set ; ::_thesis: ( a in dom p implies (G * p) . a = (h # x) . a )
assume A68: a in dom p ; ::_thesis: (G * p) . a = (h # x) . a
then reconsider n = a as Nat ;
A69: [[o, the carrier of S],(roots p)] in the Rules of (DTConMSA X) by A62, LANG1:def_1;
then reconsider rt = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
A70: len rt = len (the_arity_of o) by A69, Th5;
A71: ( (G * p) . n = G . (x . n) & (h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) ) by A64, A68, FINSEQ_3:120, MSUALG_3:def_6;
A72: h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n)) by A3;
A73: Seg (len rt) = dom rt by FINSEQ_1:def_3;
A74: ( dom rt = dom p & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def_3, TREES_3:def_18;
 p in product ((FreeSort X) * (the_arity_of o)) by A65, A60, Th1;
then A75: p . n in ((FreeSort X) * (the_arity_of o)) . n by A68, A67, A70, A73, A74, CARD_3:9;
((FreeSort X) * (the_arity_of o)) . n = the Sorts of (FreeMSA X) . ((the_arity_of o) . n) by A68, A67, A70, A73, A74, FUNCT_1:12
.= the Sorts of (FreeMSA X) . ((the_arity_of o) /. n) by A68, A70, A73, A74, PARTFUN1:def_6 ;
hence  (G * p) . a = (h # x) . a by A71, A72, A75, FUNCT_1:49; ::_thesis: verum
end;
 dom (h # x) = dom (the_arity_of o) by MSUALG_3:6;
then A76: G * p = h # x by A64, A66, FUNCT_1:2, MSUALG_3:6;
A77: h . (the_result_sort_of o) = G | ( the Sorts of (FreeMSA X) . (the_result_sort_of o)) by A3;
A78: dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o by FUNCT_2:def_1;
 (DenOp (o,X)) . p = (Sym (o,X)) -tree p by A62, Def12;
then  ( rng (DenOp (o,X)) c= ((FreeSort X) * the ResultSort of S) . o & (Sym (o,X)) -tree p in rng (DenOp (o,X)) ) by A61, A78, FUNCT_1:def_3, RELAT_1:def_19;
then  (Sym (o,X)) -tree p in ( the Sorts of (FreeMSA X) * the ResultSort of S) . o ;
then  (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . ( the ResultSort of S . o) by A59, FUNCT_1:12;
then A79: (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) by MSUALG_1:def_2;
 dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def_2;
then A80: the Sorts of (FreeMSA X) . (the_result_sort_of o) in rng the Sorts of (FreeMSA X) by FUNCT_1:def_3;
dom G = TS (DTConMSA X) by FUNCT_2:def_1
.= union (rng the Sorts of (FreeMSA X)) by Th11 ;
then A81: dom (h . (the_result_sort_of o)) = the Sorts of (FreeMSA X) . (the_result_sort_of o) by A77, A80, RELAT_1:62, ZFMISC_1:74;
Den (o,(FreeMSA X)) = (FreeOper X) . o by MSUALG_1:def_6
.= DenOp (o,X) by Def13 ;
then  (Den (o,(FreeMSA X))) . x = (Sym (o,X)) -tree p by A62, Def12;
hence (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = G . ((Sym (o,X)) -tree p) by A79, A77, A81, FUNCT_1:47
.= pi ((@ (X,(Sym (o,X)))),U1,(G * p)) by A2, A62
.= (Den (o,U1)) . (h # x) by A63, A76, Def21 ;
::_thesis: verum
end;
 for x being set st x in the carrier of S holds
(h || (FreeGen X)) . x = F . x
proof
set hf = h || (FreeGen X);
let x be set ; ::_thesis: ( x in the carrier of S implies (h || (FreeGen X)) . x = F . x )
assume  x in the carrier of S ; ::_thesis: (h || (FreeGen X)) . x = F . x
then reconsider s = x as SortSymbol of S ;
A82: dom (h . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def_1;
A83: dom ((h || (FreeGen X)) . s) = (FreeGen X) . s by FUNCT_2:def_1;
A84: (FreeGen X) . s = FreeGen (s,X) by Def16;
A85: (h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s) by Def1;
A86: for a being set st a in (FreeGen X) . s holds
((h || (FreeGen X)) . s) . a = (F . s) . a
proof
let a be set ; ::_thesis: ( a in (FreeGen X) . s implies ((h || (FreeGen X)) . s) . a = (F . s) . a )
A87: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;
assume A88: a in (FreeGen X) . s ; ::_thesis: ((h || (FreeGen X)) . s) . a = (F . s) . a
then  a in  {  (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s )  }  by A84, Th13;
then consider t being Symbol of (DTConMSA X) such that
A89: ( a = root-tree t & t in Terminals (DTConMSA X) ) and
A90: t `2 = s ;
thus ((h || (FreeGen X)) . s) . a = (h . s) . a by A85, A83, A88, FUNCT_1:47
.= G . a by A82, A84, A88, A87, FUNCT_1:47
.= pi (F, the Sorts of U1,t) by A1, A89
.= (F . s) . a by A89, A90, Def19 ; ::_thesis: verum
end;
 dom (F . s) = (FreeGen X) . s by FUNCT_2:def_1;
hence  (h || (FreeGen X)) . x = F . x by A83, A86, FUNCT_1:2; ::_thesis: verum
end;
hence  h || (FreeGen X) = F by PBOOLE:3; ::_thesis: verum
end;

theorem Th17: :: MSAFREE:17
for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free
proof
let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free
let X be V16() ManySortedSet of the carrier of S; ::_thesis: FreeMSA X is free
take  FreeGen X ; :: according to MSAFREE:def_6 ::_thesis: FreeGen X is free
thus  FreeGen X is free by Th16; ::_thesis: verum
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free for MSAlgebra over S;
existence
 ex b1 being non-empty MSAlgebra over S st
( b1 is free & b1 is strict )
proof
set U1 = the non-empty MSAlgebra over S;
set X = the Sorts of the non-empty MSAlgebra over S;
take  FreeMSA the Sorts of the non-empty MSAlgebra over S ; ::_thesis: ( FreeMSA the Sorts of the non-empty MSAlgebra over S is free & FreeMSA the Sorts of the non-empty MSAlgebra over S is strict )
thus  ( FreeMSA the Sorts of the non-empty MSAlgebra over S is free & FreeMSA the Sorts of the non-empty MSAlgebra over S is strict ) by Th17; ::_thesis: verum
end;
end;

registration
let S be non empty non void ManySortedSign ;
let U0 be free MSAlgebra over S;
cluster non empty Relation-like the carrier of S -defined Function-like total free for GeneratorSet of U0;
existence
 ex b1 being GeneratorSet of U0 st b1 is free by Def6;
end;

theorem Th18: :: MSAFREE:18
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
let U1 be non-empty MSAlgebra over S; ::_thesis: ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
set S1 = the Sorts of U1;
set FA = FreeMSA the Sorts of U1;
set FG = FreeGen the Sorts of U1;
reconsider fa = FreeMSA the Sorts of U1 as strict non-empty free MSAlgebra over S by Th17;
set f = Reverse the Sorts of U1;
take  fa ; ::_thesis: ex F being ManySortedFunction of fa,U1 st F is_epimorphism fa,U1
 FreeGen the Sorts of U1 is free by Th16;
then consider F being ManySortedFunction of (FreeMSA the Sorts of U1),U1 such that
A1: F is_homomorphism FreeMSA the Sorts of U1,U1 and
A2: F || (FreeGen the Sorts of U1) = Reverse the Sorts of U1 by Def5;
reconsider a = F as ManySortedFunction of fa,U1 ;
take  a ; ::_thesis: a is_epimorphism fa,U1
thus  a is_homomorphism fa,U1 by A1; :: according to MSUALG_3:def_8 ::_thesis: a is "onto"
thus  a is "onto" ::_thesis: verum
proof
let s be set ; :: according to MSUALG_3:def_3 ::_thesis: ( not s in the carrier of S or proj2 (a . s) = the Sorts of U1 . s )
assume  s in the carrier of S ; ::_thesis: proj2 (a . s) = the Sorts of U1 . s
then reconsider s0 = s as SortSymbol of S ;
reconsider g = a . s as Function of ( the Sorts of fa . s0),( the Sorts of U1 . s0) by PBOOLE:def_15;
A3: (Reverse the Sorts of U1) . s0 = g | ((FreeGen the Sorts of U1) . s0) by A2, Def1;
then A4: rng ((Reverse the Sorts of U1) . s0) c= rng g by RELAT_1:70;
thus  rng (a . s) c= the Sorts of U1 . s by A3, RELAT_1:def_19; :: according to XBOOLE_0:def_10 ::_thesis: the Sorts of U1 . s c= proj2 (a . s)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Sorts of U1 . s or x in proj2 (a . s) )
set D = DTConMSA the Sorts of U1;
set t = [x,s0];
assume  x in the Sorts of U1 . s ; ::_thesis: x in proj2 (a . s)
then A5: [x,s0] in Terminals (DTConMSA the Sorts of U1) by Th7;
then reconsider t = [x,s0] as Symbol of (DTConMSA the Sorts of U1) ;
 t `2 = s0 by MCART_1:7;
then  root-tree t in  {  (root-tree tt) where tt is Symbol of (DTConMSA the Sorts of U1) : ( tt in Terminals (DTConMSA the Sorts of U1) & tt `2 = s0 )  }  by A5;
then A6: root-tree t in FreeGen (s0, the Sorts of U1) by Th13;
A7: (Reverse the Sorts of U1) . s0 = Reverse (s0, the Sorts of U1) by Def18;
then  dom ((Reverse the Sorts of U1) . s0) = FreeGen (s0, the Sorts of U1) by FUNCT_2:def_1;
then A8: ((Reverse the Sorts of U1) . s0) . (root-tree t) in rng ((Reverse the Sorts of U1) . s0) by A6, FUNCT_1:def_3;
((Reverse the Sorts of U1) . s0) . (root-tree t) = t `1 by A7, A6, Def17
.= x by MCART_1:7 ;
hence  x in proj2 (a . s) by A4, A8; ::_thesis: verum
end;
end;

theorem :: MSAFREE:19
for S being non empty non void ManySortedSign
for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
let U1 be strict non-empty MSAlgebra over S; ::_thesis: ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )
consider U0 being strict non-empty free MSAlgebra over S, F being ManySortedFunction of U0,U1 such that
A1: F is_epimorphism U0,U1 by Th18;
 F is_homomorphism U0,U1 by A1, MSUALG_3:def_8;
then  Image F = U1 by A1, MSUALG_3:19;
hence  ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 ) by A1; ::_thesis: verum
end;