The Mizar article:

Free Many Sorted Universal Algebra

by
Beata Perkowska

Received April 27, 1994

Copyright (c) 1994 Association of Mizar Users

MML identifier: MSAFREE
[ MML identifier index ]


environ

 vocabulary FUNCT_1, PBOOLE, TDGROUP, CARD_3, RELAT_1, MSUALG_2, PRALG_1,
      REALSET1, BOOLE, ZF_REFLE, PROB_1, TARSKI, AMI_1, MSUALG_1, FREEALG,
      PRELAMB, ALG_1, FINSEQ_1, QC_LANG1, LANG1, DTCONSTR, TREES_4, TREES_2,
      TREES_3, FUNCT_6, MCART_1, UNIALG_2, GROUP_6, MSUALG_3, MSAFREE,
      FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, RELAT_1,
      RELSET_1, STRUCT_0, FUNCT_1, MCART_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
      TREES_2, PROB_1, CARD_3, FINSEQ_4, LANG1, TREES_3, FUNCT_6, TREES_4,
      DTCONSTR, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3;
 constructors NAT_1, MCART_1, MSUALG_3, FINSOP_1, FINSEQ_4, FINSEQOP, PROB_1,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSEQ_1, PBOOLE, TREES_3, TREES_4, DTCONSTR,
      PRALG_1, MSUALG_1, MSUALG_3, RELSET_1, STRUCT_0, XBOOLE_0, ARYTM_3,
      MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3, STRUCT_0;
 theorems TARSKI, FUNCT_1, FUNCT_2, MCART_1, ZFMISC_1, PBOOLE, CARD_3,
      MSUALG_1, MSUALG_2, MSUALG_3, PRALG_1, RELAT_1, LANG1, DTCONSTR,
      FINSEQ_1, TREES_4, FINSEQ_4, TREES_1, TREES_2, ALG_1, DOMAIN_1, PROB_1,
      RELSET_1, XBOOLE_0, XBOOLE_1;
 schemes ZFREFLE1, FUNCT_1, RELSET_1, MSUALG_2, DTCONSTR, COMPTS_1, XBOOLE_0;

begin

::
:: Preliminaries
::

theorem Th1:
for I be set, J be non empty set, f be Function of I,J*,
    X be ManySortedSet of J, p be Element of J*, x be set
st x in I & p = f.x holds (X# * f).x = product (X * p)
 proof
  let I be set,
      J be non empty set,
      f be Function of I,J*,
      X be ManySortedSet of J,
      p be Element of J*,
      x be set;
  assume A1: x in I & p = f.x;
  A2: dom f = I & rng f c= J* by FUNCT_2:def 1,RELSET_1:12;
  then dom (X# * f) = dom f by PBOOLE:def 3;
  hence (X# * f).x =(X# qua ManySortedSet of J*).p by A1,A2,FUNCT_1:22
  .= product (X * p) by MSUALG_1:def 3;
 end;

definition
 let I be set,
     A,B be ManySortedSet of I,
     C be ManySortedSubset of A,
     F be ManySortedFunction of A,B;
func F || C -> ManySortedFunction of C,B means :Def1:
for i be set st i in I
 for f be Function of A.i,B.i st f = F.i holds it.i = f | (C.i);
existence
 proof
  defpred P[set,set] means
  for f be Function of A.$1,B.$1 st f = F.$1 holds $2 = f | (C.$1);
  A1: for i be set st i in I ex u be set st P[i,u]
   proof
    let i be set;
    assume i in I;
    then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
    take f | (C.i);
    thus thesis;
   end;
  consider H be Function such that
  A2: dom H = I & for i be set st i in I holds P[i,H.i] from NonUniqFuncEx(A1);
  reconsider H as ManySortedSet of I by A2,PBOOLE:def 3;
    for i be set st i in I holds H.i is Function of C.i,B.i
    proof
     let i be set;
     assume A3: i in I;
     then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
     A4: H.i = f | (C.i) by A2,A3;
       C c= A by MSUALG_2:def 1;
     then A5: C.i c= A.i by A3,PBOOLE:def 5;
     per cases;
     suppose
     A6: B.i is empty;
     set h = f | (C.i);
       rng h c= B.i by RELSET_1:12;
     then rng h = {} by A6,XBOOLE_1:3;
     then A7:   H.i = {} by A4,RELAT_1:64;
       now per cases;
      suppose C.i = {};
        hence thesis by A7,FUNCT_2:55,RELAT_1:60;
      suppose
        C.i <> {};
        hence thesis by A6,A7,FUNCT_2:def 1,RELSET_1:25;
     end;
     hence thesis;
     suppose
     A8: B.i is non empty;
     then A9: dom f = A.i & rng f c= B.i by FUNCT_2:def 1,RELSET_1:12;
     A10: dom (f|(C.i)) = dom f /\ (C.i) by FUNCT_1:68
     .= C.i by A5,A9,XBOOLE_1:28;
       rng (f|(C.i)) c= B.i by RELSET_1:12;
     hence thesis by A4,A8,A10,FUNCT_2:def 1,RELSET_1:11;
    end;
  then reconsider H as ManySortedFunction of C,B by MSUALG_1:def 2;
  take H;
  thus thesis by A2;
 end;
uniqueness
 proof
  let X,Y be ManySortedFunction of C,B;assume that
  A11: for i be set st i in I
      for f be Function of A.i,B.i st f = F.i holds X.i = f | (C.i) and
  A12: for i be set st i in I
      for f be Function of A.i,B.i st f = F.i holds Y.i = f | (C.i);
    for i be set st i in I holds X.i = Y.i
    proof
     let i be set;
     assume A13: i in I;
     then reconsider f = F.i as Function of A.i,B.i by MSUALG_1:def 2;
       X.i = f|(C.i) & Y.i = f|(C.i) by A11,A12,A13;
     hence thesis;
    end;
  hence thesis by PBOOLE:3;
 end;
end;

definition let I be set,
               X be ManySortedSet of I,
               i be set;
 assume A1: i in I;
func coprod(i,X) -> set means :Def2:
for x be set holds x in it iff ex a be set st a in X.i & x = [a,i];
 existence
  proof
   defpred P[set] means ex a be set st a in X.i & $1 = [a,i];
   consider A be set such that
   A2: for x be set holds x in A iff
      x in [:X.i,I:] & P[x] from Separation;
   take A;
   let x be set;
   thus x in A implies ex a be set st a in X.i & x = [a,i] by A2;
   given a be set such that
   A3: a in X.i & x = [a,i];
     x in [:X.i,I:] by A1,A3,ZFMISC_1:106;
   hence thesis by A2,A3;
  end;
 uniqueness
  proof
   let A,B be set;assume that
   A4: for x be set holds x in A iff ex a be set st a in X.i & x = [a,i] and
   A5: for x be set holds x in B iff ex a be set st a in X.i & x = [a,i];
   thus A c= B
    proof
     let x be set;
     assume x in A;
     then ex a be set st a in X.i & x = [a,i] by A4;
     hence thesis by A5;
    end;
   let x be set;
   assume x in B;
   then ex a be set st a in X.i & x = [a,i] by A5;
   hence thesis by A4;
  end;
end;

definition let I be set,
               X be ManySortedSet of I;
 redefine func disjoin X -> ManySortedSet of I means :Def3:
   for i be set st i in I holds it.i = coprod(i,X);
 coherence
  proof
      dom X = I by PBOOLE:def 3;
   hence dom disjoin X = I by CARD_3:def 3;
  end;
 compatibility
  proof let IT be ManySortedSet of I;
   hereby assume
A1:   IT = disjoin X;
    let i be set;
    assume
A2:  i in I;
     then i in dom X by PBOOLE:def 3;
then A3:  IT.i = [:X.i,{i}:] by A1,CARD_3:def 3;
       now let x be set;
      hereby assume x in IT.i;
        then consider a,b being set such that
A4:      a in X.i & b in {i} and
A5:     x = [a,b] by A3,ZFMISC_1:def 2;
       take a;
       thus a in X.i by A4;
       thus x = [a,i] by A4,A5,TARSKI:def 1;
      end;
      given a being set such that
A6:    a in X.i and
A7:    x = [a,i];
         i in {i} by TARSKI:def 1;
      hence x in IT.i by A3,A6,A7,ZFMISC_1:def 2;
     end;
    hence IT.i = coprod(i,X) by A2,Def2;
   end;
   assume
A8:  for i be set st i in I holds IT.i = coprod(i,X);
A9:  dom IT = I by PBOOLE:def 3;
    then A10:  dom IT = dom X by PBOOLE:def 3;
     now let x be set;
    assume
A11:  x in dom X;
then A12:  x in I by PBOOLE:def 3;
A13:   now let a be set;
      hereby assume a in coprod(x,X);
        then consider b being set such that
A14:     b in X.x and
A15:     a = [b,x] by A12,Def2;
          x in {x} by TARSKI:def 1;
       hence a in [:X.x,{x}:] by A14,A15,ZFMISC_1:def 2;
      end;
      assume a in [:X.x,{x}:];
       then consider a1,a2 being set such that
A16:     a1 in X.x & a2 in {x} and
A17:     a = [a1,a2] by ZFMISC_1:def 2;
         a2 = x by A16,TARSKI:def 1;
      hence a in coprod(x,X) by A12,A16,A17,Def2;
     end;
    thus IT.x = coprod(x,X) by A8,A9,A10,A11
             .= [:X.x,{x}:] by A13,TARSKI:2;
   end;
   hence IT = disjoin X by A10,CARD_3:def 3;
  end;
 synonym coprod X;
end;

definition
 let I be non empty set,
     X be non-empty ManySortedSet of I;
 cluster coprod X -> non-empty;
coherence
 proof
     now
    let x be set;
    assume x in I;
    then reconsider i = x as Element of I;
    A1: (coprod X).i = coprod(i,X) by Def3;
    consider a be set such that
    A2: a in X.i by XBOOLE_0:def 1;
      [a,i] in (coprod X).i by A1,A2,Def2;
    hence (coprod X).x is non empty;
   end;
  hence thesis by PBOOLE:def 16;
 end;
end;

definition
 let I be non empty set,
     X be non-empty ManySortedSet of I;
 cluster Union X -> non empty;
coherence
 proof
  consider i be Element of I;
  consider a be set such that
  A1: a in X.i by XBOOLE_0:def 1;
    dom X = I by PBOOLE:def 3;
  then X.i in rng X by FUNCT_1:def 5;
  then a in union rng X by A1,TARSKI:def 4;
  hence thesis by PROB_1:def 3;
 end;
end;

theorem
  for I be set, X be ManySortedSet of I, i be set st i in I holds
X.i <> {} iff (coprod X).i <> {}
 proof
  let I be set,
      X be ManySortedSet of I,
      i be set;
  assume A1: i in I;
  then A2: (coprod X).i = coprod(i,X) by Def3;
  thus X.i <> {} implies (coprod X).i <> {}
   proof
    assume X.i <> {};
    then consider x be 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 thesis;
   end;
  assume (coprod X).i <> {};
  then consider a be set such that A4: a in coprod(i,X) by A2,XBOOLE_0:def 1;
  consider x be set such that A5: x in X.i & a = [x,i] by A1,A4,Def2;
  thus thesis by A5;
 end;

begin
::
:: Free Many Sorted Universal Algebra - General Notions
::

reserve S for non void non empty ManySortedSign,
        U0 for MSAlgebra over S;

definition
 let S be non void non empty ManySortedSign,
     U0 be MSAlgebra over S;
mode GeneratorSet of U0 -> MSSubset of U0 means :Def4:
the Sorts of GenMSAlg(it) = the Sorts of U0;
 existence
  proof
   set A = the Sorts of U0;
   reconsider A as MSSubset of U0 by MSUALG_2:def 1;
   take A;
   set G = GenMSAlg(A);
     A is MSSubset of G by MSUALG_2:def 18;
   then A1: A c= the Sorts of G by MSUALG_2:def 1;
     the Sorts of G is MSSubset of U0 by MSUALG_2:def 10;
   then the Sorts of G c= A by MSUALG_2:def 1;
   hence thesis by A1,PBOOLE:def 13;
  end;
end;

theorem
  for S be non void non empty ManySortedSign,
    U0 be strict non-empty MSAlgebra over S,
    A be MSSubset of U0 holds
          A is GeneratorSet of U0 iff GenMSAlg(A) = U0
 proof
  let S be non void non empty ManySortedSign,
     U0 be strict non-empty MSAlgebra over S,
      A be MSSubset of U0;
  thus A is GeneratorSet of U0 implies GenMSAlg(A) = U0
   proof
    assume A1: A is GeneratorSet of U0;
    reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:6;
      the Sorts of GenMSAlg(A) = the Sorts of U1 by A1,Def4;
    hence thesis by MSUALG_2:10;
   end;
   assume GenMSAlg(A) = U0;
   hence thesis by Def4;
 end;

definition
 let S,U0;
 let IT be GeneratorSet of U0;
attr IT is free means :Def5:
for U1 be non-empty MSAlgebra over S
 for f be ManySortedFunction of IT,the Sorts of U1
  ex h be ManySortedFunction of U0,U1
                  st h is_homomorphism U0,U1 & h || IT = f;
end;

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

theorem Th4:
for S be non void non empty ManySortedSign,
    X be ManySortedSet of the carrier of S
holds Union coprod X misses [:the OperSymbols of S,{the carrier of S}:]
 proof
  let S be non void non empty ManySortedSign,
      X be ManySortedSet of the carrier of S;
  assume Union (coprod X) /\ [:the OperSymbols of S,{the carrier of S}:] <> {}
;
   then consider x be set such that
  A1: x in Union (coprod X) /\ [:the OperSymbols of S,{the carrier of S}:]
                  by XBOOLE_0:def 1;
  A2: x in Union (coprod X) & x in [:the OperSymbols of S,{the carrier of S}:]
                by A1,XBOOLE_0:def 3;
  then x in union rng (coprod X) by PROB_1:def 3;
  then consider A be set such that
  A3: x in A & A in rng (coprod X) by TARSKI:def 4;
  consider s be set such that
  A4: s in dom (coprod X) & (coprod X).s = A by A3,FUNCT_1:def 5;
  reconsider s as SortSymbol of S by A4,PBOOLE:def 3;
A5: s in the carrier of S;
    A = coprod(s,X) by A4,Def3;
  then consider a be set such that
  A6: a in X.s & x = [a,s] by A3,Def2;
    s in {the carrier of S} by A2,A6,ZFMISC_1:106;
  then s = the carrier of S by TARSKI:def 1;
  hence contradiction by A5;
 end;

begin
::
:: Construction of Free Many Sorted Algebras for Given Signature
::

definition
 let S be non void ManySortedSign;
 cluster the OperSymbols of S -> non empty;
 coherence by MSUALG_1:def 5;
end;

definition
 let S be non void non empty ManySortedSign,
     X be ManySortedSet of the carrier of S;
 canceled 2;

func REL(X) -> Relation of
   ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)),
   (([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*) means
:Def9:
for a be Element of
        [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X),
    b be Element of
       ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
 holds
 [a,b] in it iff
  a in [:the OperSymbols of S,{the carrier of S}:] &
  for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
    for o1 be 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
  proof
   set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
   defpred P[Element of O,Element of O*]
   means $1 in [:the OperSymbols of S,{the carrier of S}:] &
   for o be OperSymbol of S st [o,the carrier of S] = $1 holds
   len $2 = len (the_arity_of o) &
   for x be set st x in dom $2 holds
    ($2.x in [:the OperSymbols of S,{the carrier of S}:] implies
      for o1 be 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 be Relation of O,O* such that
   A1: for a be Element of O, b be Element of O* holds [a,b] in R iff
       P[a,b] from Rel_On_Dom_Ex;
   take R;
   let a be Element of O, b be Element of O*;
   thus [a,b] in R implies a in [:the OperSymbols of S,{the carrier of S}:] &
   for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be 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;
   assume a in [:the OperSymbols of S,{the carrier of S}:] &
   for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
    for o1 be 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));
   hence thesis by A1;
  end;
 uniqueness
  proof
   set O = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
   let R,P be Relation of O,O*;
   assume that
   A2: for a be Element of O, b be Element of O* holds [a,b] in R iff
  a in [:the OperSymbols of S,{the carrier of S}:] &
  for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be 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 be Element of O, b be Element of O* holds [a,b] in P iff
  a in [:the OperSymbols of S,{the carrier of S}:] &
  for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
   for o1 be 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 x,y be set holds [x,y] in R iff [x,y] in P
    proof
     let x,y be set;
     thus [x,y] in R implies [x,y] in P
      proof
       assume A4: [x,y] in R;
       then reconsider a = x as Element of O by ZFMISC_1:106;
       reconsider b = y as Element of O* by A4,ZFMISC_1:106;
         [a,b] in R by A4;
  then a in [:the OperSymbols of S,{the carrier of S}:] &
  for o be OperSymbol of S st [o,the carrier of S] = a holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be 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;
       hence thesis by A3;
      end;
     assume A5: [x,y] in P;
     then reconsider a = x as Element of O by ZFMISC_1:106;
     reconsider b = y as Element of O* by A5,ZFMISC_1:106;
       [a,b] in P by A5;
     then a in [:the OperSymbols of S,{the carrier of S}:] &
     for o be OperSymbol of S st [o,the carrier of S] = a holds
     len b = len (the_arity_of o) &
     for x be set st x in dom b holds
     (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be 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;
       hence thesis by A2;
    end;
   hence thesis by RELAT_1:def 2;
  end;
end;

reserve S for non void non empty ManySortedSign,
         X for ManySortedSet of the carrier of S,
         o for OperSymbol of S,
         b for Element of
            ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
;

theorem Th5:
               [[o,the carrier of S],b] in REL(X)
                            iff
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be 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
  defpred
    P[OperSymbol of S,Element of
        ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*]
    means len $2 = len (the_arity_of $1) &
   for x be set st x in dom $2 holds
    ($2.x in [:the OperSymbols of S,{the carrier of S}:] implies
    for o1 be 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: a in [:the OperSymbols of S,{the carrier of S}:] by ZFMISC_1:106;
  then reconsider a as Element of
       [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
     by XBOOLE_0:def 2;
  thus [[o,the carrier of S],b] in REL(X) implies P[o,b]
   proof
    assume [[o,the carrier of S],b] in REL(X);
    then for o1 be OperSymbol of S st [o1,the carrier of S] = a
           holds P[o1,b] by Def9;
    hence thesis;
   end;
  assume
A2:  P[o,b];
     now let o1 be OperSymbol of S;
    assume [o1,the carrier of S] = a;
     then o1 = o by ZFMISC_1:33;
    hence P[o1,b] by A2;
   end;
   hence thesis by A1,Def9;
 end;

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

definition
 let S be non void non empty ManySortedSign,
     X be ManySortedSet of the carrier of S;
 cluster DTConMSA(X) -> strict non empty;
 coherence
  proof
      DTConMSA(X) = DTConstrStr (# [:the OperSymbols of S,{the carrier of S}:]
                   \/ Union (coprod X), REL(X) #) by Def10;
   hence DTConMSA X is strict & the carrier of DTConMSA(X) is non empty;
  end;
end;

theorem Th6:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S holds
NonTerminals(DTConMSA(X)) = [:the OperSymbols of S,{the carrier of S}:] &
Terminals (DTConMSA(X)) = Union (coprod X)
  proof
   let S be non void non empty ManySortedSign,
       X be non-empty ManySortedSet of the carrier of S;
   A1: Union(coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
         by Th4;
   set D = DTConMSA(X),
       A = [:the OperSymbols of S,{the carrier of S}:] \/
           Union (coprod (X qua ManySortedSet of the carrier of S));
   A2: D = DTConstrStr (# A , REL(X) #) by Def10;
   A3: the carrier of D = (Terminals D) \/ (NonTerminals D) &
      (Terminals D) misses (NonTerminals D) by DTCONSTR:8,LANG1:1;
  thus
A4: NonTerminals D c= [:the OperSymbols of S,{the carrier of S}:]
   proof
    let x be set;
    assume x in NonTerminals D;
    then x in { s where s is Symbol of D: ex n being FinSequence st s ==> n}
                                             by LANG1:def 3;
    then consider s be Symbol of D such that
    A5: s = x & ex n being FinSequence st s ==> n;
    consider n be FinSequence such that
    A6: s ==> n by A5;
    A7: [s,n] in the Rules of D by A6,LANG1:def 1;
    reconsider s as Element of A by A2;
    reconsider n as Element of A* by A2,A7,ZFMISC_1:106;
      [s,n] in REL X by A2,A6,LANG1:def 1;
    hence thesis by A5,Def9;
   end;
   thus
A8:  [:the OperSymbols of S,{the carrier of S}:] c= NonTerminals D
    proof
     let x be set; assume
A9:   x in [:the OperSymbols of S,{the carrier of S}:];
     then consider o being OperSymbol of S, x2 being Element of {the carrier of
S}
     such that
A10:   x = [o,x2] by DOMAIN_1:9;
A11:   the carrier of S = x2 by TARSKI:def 1;
     then reconsider xa = [o,the carrier of S]
       as Element of (the carrier of D) by A2,A9,A10,XBOOLE_0:def 2;
     set O = the_arity_of o;
     defpred P[set,set] means $2 in coprod (O.$1,X);
     A12: for a be set st a in Seg len O ex b be set st P[a,b]
      proof
       let a be set; assume
         a in Seg len O;
       then a in dom O by FINSEQ_1:def 3;
       then A13: O.a in rng O & rng O c= the carrier of S
                    by FINSEQ_1:def 4,FUNCT_1:def 5;
       then X.(O.a) is non empty by PBOOLE:def 16;
       then consider x be set such that
       A14: x in X.(O.a) by XBOOLE_0:def 1;
       take y = [x,O.a];
       thus y in coprod(O.a,X) by A13,A14,Def2;
      end;
     consider b be Function such that
     A15: dom b = Seg len O &
     for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A12);
     reconsider b as FinSequence by A15,FINSEQ_1:def 2;
       rng b c= A
      proof let a be set; assume a in rng b;
       then consider c be set such that
       A16: c in dom b & b.c = a by FUNCT_1:def 5;
       A17: a in coprod(O.c,X) by A15,A16;
         dom O = Seg len O by FINSEQ_1:def 3;
       then A18: O.c in rng O & rng O c= the carrier of S
           by A15,A16,FINSEQ_1:def 4,FUNCT_1:def 5;
         dom coprod(X) = the carrier of S by PBOOLE:def 3;
       then (coprod(X)).(O.c) in rng coprod(X) by A18,FUNCT_1:def 5;
       then coprod(O.c,X) in rng coprod(X) by A18,Def3;
       then a in union rng coprod(X) by A17,TARSKI:def 4;
       then a in Union coprod(X) by PROB_1:def 3;
       hence thesis by XBOOLE_0:def 2;
      end;
     then reconsider b as FinSequence of A by FINSEQ_1:def 4;
     reconsider b as Element of A* by FINSEQ_1:def 11;
     A19: len b = len O by A15,FINSEQ_1:def 3;
        now let c be set;
       assume A20: c in dom b;
       then A21: P[c,b.c] by A15;
         dom O = Seg len O by FINSEQ_1:def 3;
       then A22: O.c in rng O & rng O c= the carrier of S
           by A15,A20,FINSEQ_1:def 4,FUNCT_1:def 5;
         dom coprod(X) = the carrier of S by PBOOLE:def 3;
       then (coprod(X)).(O.c) in rng coprod(X) by A22,FUNCT_1:def 5;
       then coprod(O.c,X) in rng coprod(X) by A22,Def3;
       then b.c in union rng coprod(X) by A21,TARSKI:def 4;
       then b.c in Union coprod(X) by PROB_1:def 3;
       hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies
        for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds
       the_result_sort_of o1 = O.c by A1,XBOOLE_0:3;
       assume b.c in Union (coprod X);
       thus b.c in coprod(O.c,X) by A15,A20;
      end;
     then [xa,b] in REL(X) by A19,Th5;
     then xa ==> b by A2,LANG1:def 1;
     then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n};
     hence thesis by A10,A11,LANG1:def 3;
    end;
   thus Terminals D c= Union (coprod X)
      proof
       let x be set; assume A23: x in Terminals D;
       then A24: x in A by A2,A3,XBOOLE_0:def 2;
          not x in [:the OperSymbols of S,{the carrier of S}:]
          by A3,A8,A23,XBOOLE_0:3;
       hence thesis by A24,XBOOLE_0:def 2;
      end;
   let x be set; assume A25: x in Union (coprod X);
    then x in A by XBOOLE_0:def 2;
     then x in Terminals D or x in NonTerminals D by A2,A3,XBOOLE_0:def 2;
   hence thesis by A1,A4,A25,XBOOLE_0:3;
  end;

reserve x for set;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
cluster DTConMSA(X) -> with_terminals with_nonterminals
   with_useful_nonterminals;
 coherence
  proof
   set D = DTConMSA(X),
       A = [:the OperSymbols of S,{the carrier of S}:] \/
            Union (coprod (X qua ManySortedSet of the carrier of S));
   A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
        by Th4;
   A2: Terminals D = Union (coprod X) &
       NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th6;
   A3: D = DTConstrStr (# A , REL(X) #) by Def10;
    for nt being Symbol of D st nt in NonTerminals D
   ex p being FinSequence of TS(D) st nt ==> roots p
   proof
    let nt be Symbol of D;
    assume nt in NonTerminals D;
     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:9;
A5:   the carrier of S = x2 by TARSKI:def 1;
    set O = the_arity_of o;
    defpred P[set,set] means $2 in coprod(O.$1,X);
    A6: for a be set st a in Seg len O ex b be set st P[a,b]
     proof
      let a be set; assume
        a in Seg len O;
      then a in dom O by FINSEQ_1:def 3;
      then A7: O.a in
 rng O & rng O c= the carrier of S by FINSEQ_1:def 4,FUNCT_1:def 5;
      then X.(O.a) is non empty by PBOOLE:def 16;
      then consider x be set such that
      A8: x in X.(O.a) by XBOOLE_0:def 1;
      take y = [x,O.a];
      thus y in coprod(O.a,X) by A7,A8,Def2;
     end;
    consider b be Function such that
    A9: dom b = Seg len O &
    for a be set st a in Seg len O holds P[a,b.a] from NonUniqFuncEx(A6);
    reconsider b as FinSequence by A9,FINSEQ_1:def 2;
    A10: rng b c= A
     proof let a be set; assume a in rng b;
      then consider c be set such that
      A11: c in dom b & b.c = a by FUNCT_1:def 5;
      A12: a in coprod (O.c,X) by A9,A11;
        dom O = Seg len O by FINSEQ_1:def 3;
      then A13: O.c in rng O & rng O c= the carrier of S
                                 by A9,A11,FINSEQ_1:def 4,FUNCT_1:def 5;
        dom coprod(X) = the carrier of S by PBOOLE:def 3;
      then (coprod(X)).(O.c) in rng coprod(X) by A13,FUNCT_1:def 5;
      then coprod(O.c,X) in rng coprod(X) by A13,Def3;
      then a in union rng coprod(X) by A12,TARSKI:def 4;
      then a in Union coprod(X) by PROB_1:def 3;
      hence thesis by XBOOLE_0:def 2;
     end;
    then reconsider b as FinSequence of A by FINSEQ_1:def 4;
    reconsider b as Element of A* by FINSEQ_1:def 11;
    A14: len b = len O by A9,FINSEQ_1:def 3;
       now let c be set;
      assume A15: c in dom b;
      then A16: P[c,b.c] by A9;
        dom O = Seg len O by FINSEQ_1:def 3;
      then A17: O.c in rng O & rng O c= the carrier of S
                               by A9,A15,FINSEQ_1:def 4,FUNCT_1:def 5;
        dom coprod(X) = the carrier of S by PBOOLE:def 3;
      then (coprod(X)).(O.c) in rng coprod(X) by A17,FUNCT_1:def 5;
      then coprod(O.c,X) in rng coprod(X) by A17,Def3;
      then b.c in union rng coprod(X) by A16,TARSKI:def 4;
       then b.c in Union coprod(X) by PROB_1:def 3;
      hence b.c in [:the OperSymbols of S,{the carrier of S}:] implies
      for o1 be OperSymbol of S st [o1,the carrier of S] = b.c holds
      the_result_sort_of o1 = O.c by A1,XBOOLE_0:3;
      assume b.c in Union (coprod X);
      thus b.c in coprod(O.c,X) by A9,A15;
     end;
     then [nt,b] in REL(X) by A4,A5,A14,Th5;
    then A18: nt ==> b by A3,LANG1:def 1;
    deffunc F(set)=root-tree (b.$1);
    consider f be Function such that
    A19: dom f = dom b & for x st x in dom b holds f.x = F(x)
                                                        from Lambda;
    reconsider f as FinSequence by A9,A19,FINSEQ_1:def 2;
      rng f c= TS(D)
     proof
      let x;
      assume x in rng f;
      then consider y be set such that
      A20: y in dom f & f.y = x by FUNCT_1:def 5;
      A21: x = root-tree(b.y) by A19,A20;
        b.y in rng b by A19,A20,FUNCT_1:def 5;
      then reconsider a = b.y as Symbol of D by A3,A10;
      A22: P[y,b.y] by A9,A19,A20;
        dom O = Seg len O by FINSEQ_1:def 3;
      then A23: O.y in rng O & rng O c= the carrier of S
                               by A9,A19,A20,FINSEQ_1:def 4,FUNCT_1:def 5;
        dom coprod(X) = the carrier of S by PBOOLE:def 3;
      then (coprod(X)).(O.y) in rng coprod(X) by A23,FUNCT_1:def 5;
      then coprod(O.y,X) in rng coprod(X) by A23,Def3;
      then b.y in union rng coprod(X) by A22,TARSKI:def 4;
      then a in Terminals D by A2,PROB_1:def 3;
      hence thesis by A21,DTCONSTR:def 4;
     end;
    then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
    take f;
    A24: dom (roots f) = dom f by DTCONSTR:def 1;
      for x st x in dom b holds (roots f).x = b.x
     proof
      let x;
      assume A25: x in dom b;
      then A26: f.x = root-tree (b.x) by A19;
      reconsider i = x as Nat by A25;
      consider T be DecoratedTree such that
      A27: T = f.i & (roots f).i = T.{} by A19,A25,DTCONSTR:def 1;
      thus thesis by A26,A27,TREES_4:3;
     end;
    hence thesis by A18,A19,A24,FUNCT_1:9;
   end;
   hence thesis by A2,DTCONSTR:def 6,def 7,def 8;
  end;
end;

theorem Th7:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S,
    t be set holds
               t in Terminals DTConMSA(X)
                          iff
 ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]
 proof
  let S be non void non empty ManySortedSign,
      X be non-empty ManySortedSet of the carrier of S,
      t be set;
  set D = DTConMSA(X);
  A1: Terminals D = Union (coprod X) by Th6
                 .= union rng (coprod X) by PROB_1:def 3;
  thus t in Terminals D implies
       ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]
   proof
    assume t in Terminals D;
    then consider A be set such that
    A2: t in A & A in rng(coprod X) by A1,TARSKI:def 4;
    consider s be set such that
    A3: s in dom (coprod X) & (coprod X).s = A by A2,FUNCT_1:def 5;
    reconsider s as SortSymbol of S by A3,PBOOLE:def 3;
    take s;
      (coprod X).s = coprod(s,X) by Def3;
    then consider x be set such that
    A4: x in X.s & t = [x,s] by A2,A3,Def2;
    take x;
    thus thesis by A4;
   end;
  given s be SortSymbol of S, x be set such that
  A5: x in X.s & t = [x,s];
    t in coprod(s,X) by A5,Def2;
  then A6: t in (coprod X).s by Def3;
    dom(coprod X) = the carrier of S by PBOOLE:def 3;
  then (coprod X).s in rng (coprod X) by FUNCT_1:def 5;
  hence thesis by A1,A6,TARSKI:def 4;
 end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     o be OperSymbol of S;
func Sym(o,X) ->Symbol of DTConMSA(X) equals :Def11:
 [o,the carrier of S];
 coherence
  proof
     the carrier of S in {the carrier of S} by TARSKI:def 1;
   then [o,the carrier of S] in [:the OperSymbols of S,{the carrier of S}:]
                by ZFMISC_1:106;
    then [o,the carrier of S] in NonTerminals (DTConMSA X) by Th6;
   hence [o,the carrier of S] is Symbol of DTConMSA(X);
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     s be SortSymbol of S;
func FreeSort(X,s) -> Subset of TS(DTConMSA(X)) equals :Def12:
 {a where a is Element of TS(DTConMSA(X)):
       (ex x be set st x in X.s & a = root-tree [x,s]) or
       ex o be OperSymbol of S st [o,the carrier of S] = a.{}
           & the_result_sort_of o = s};
 coherence
  proof
   set A = {a where a is Element of TS(DTConMSA(X)):
            (ex x be set st x in X.s & a = root-tree [x,s]) or
             ex o be OperSymbol of S st [o,the carrier of S] = a.{}
                  & the_result_sort_of o = s};
     A c= TS(DTConMSA(X))
    proof
     let x be set;
     assume x in A;
     then consider a be Element of TS(DTConMSA(X)) such that A1: x = a and
              (ex x be set st x in X.s & a = root-tree [x,s]) or
             ex o be OperSymbol of S st [o,the carrier of S] = a.{}
                  & the_result_sort_of o = s;
     thus thesis by A1;
    end;
    hence thesis;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     s be SortSymbol of S;
cluster FreeSort(X,s) -> non empty;
 coherence
  proof
   set A = {a where a is Element of TS(DTConMSA(X)):
            (ex x be set st x in X.s & a = root-tree [x,s]) or
             ex o be OperSymbol of S st [o,the carrier of S] = a.{}
                  & the_result_sort_of o = s};
   consider x be set such that A1: x in X.s by XBOOLE_0:def 1;
   set a = [x,s];
   A2: a in coprod(s,X) by A1,Def2;
   A3: (Terminals (DTConMSA(X))) = Union (coprod X) by Th6;
     dom coprod(X) = the carrier of S by PBOOLE:def 3;
   then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5;
   then coprod(s,X) in rng coprod(X) by Def3;
   then a in union rng coprod(X) by A2,TARSKI:def 4;
   then A4: a in Terminals (DTConMSA X) by A3,PROB_1:def 3;
   then reconsider a as Symbol of DTConMSA(X);
   reconsider b = root-tree a as Element of TS(DTConMSA X)
                                                  by A4,DTCONSTR:def 4;
     b in A by A1;
   hence thesis by Def12;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
func FreeSort(X) -> ManySortedSet of the carrier of S means :Def13:
for s be SortSymbol of S holds it.s = FreeSort(X,s);
 existence
  proof
   deffunc F(Element of S)=FreeSort(X,$1);
   consider f be Function such that
   A1: dom f = the carrier of S &
   for d be Element of S holds f.d =F(d)  from LambdaB;
   reconsider f as ManySortedSet of the carrier of S by A1,PBOOLE:def 3;
   take f;
   thus thesis by A1;
  end;
 uniqueness
  proof
   let A,B be ManySortedSet of the carrier of S;
   assume that A2: for s be SortSymbol of S holds A.s = FreeSort(X,s) and
          A3: for s be SortSymbol of S holds B.s = FreeSort(X,s);
     for i be set st i in the carrier of S holds A.i = B.i
    proof
     let i be set;
     assume i in the carrier of S;
     then reconsider s = i as SortSymbol of S;
       A.s = FreeSort(X,s) & B.s = FreeSort(X,s) by A2,A3;
     hence thesis;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
cluster FreeSort(X) -> non-empty;
coherence
  proof
   let i be set;
   assume i in the carrier of S;
   then reconsider s = i as SortSymbol of S;
     (FreeSort(X)).s = FreeSort(X,s) by Def13;
   hence thesis;
  end;
end;

theorem Th8:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S,
    x be set
 st x in ((FreeSort X)# * (the Arity of S)).o holds
    x is FinSequence of TS(DTConMSA(X))
 proof
  let S be non void non empty ManySortedSign,
      X be non-empty ManySortedSet of the carrier of S,
      o be OperSymbol of S,
      x be set;
   assume A1: x in ((FreeSort X)# * (the Arity of S)).o;
   set D = DTConMSA(X),
      ar = the_arity_of o,
      cr = the carrier of S;
     (the Arity of S).o = ar by MSUALG_1:def 6;
   then x in product ((FreeSort X) * ar) by A1,Th1;
   then consider f be Function such that
   A2: x = f & dom f = dom ((FreeSort X) * ar) &
    for y be set st y in dom ((FreeSort X)* ar)
       holds f.y in ((FreeSort X) * ar).y by CARD_3:def 5;
   A3: rng ar c= cr by FINSEQ_1:def 4;
     dom ((FreeSort X)) = cr by PBOOLE:def 3;
   then A4: dom ((FreeSort X) * ar) = dom ar by A3,RELAT_1:46;
     dom ar = Seg len ar by FINSEQ_1:def 3;
   then reconsider f as FinSequence by A2,A4,FINSEQ_1:def 2;
     rng f c= TS D
    proof
     let a be set; assume a in rng f;
     then consider b be set such that
     A5: b in dom f & f.b = a by FUNCT_1:def 5;
     A6: a in ((FreeSort X) * ar).b by A2,A5;
     reconsider b as Nat by A5;
       ((FreeSort X) * ar).b = (FreeSort X).(ar.b) by A2,A5,FUNCT_1:22
     .= (FreeSort X). (ar/.b) by A2,A4,A5,FINSEQ_4:def 4
     .= FreeSort(X,ar/.b) by Def13
     .= { s where s is Element of TS D:
       (ex x be set st x in X.(ar/.b) & s = root-tree [x,ar/.b]) or
       ex o1 be OperSymbol of S st
        [o1,the carrier of S] = s.{} & the_result_sort_of o1=ar/.b}
             by Def12;
     then consider e be Element of TS D such that
     A7: a = e and
       (ex x be set st x in X.(ar/.b) & e = root-tree [x,(ar/.b)]) or
     ex o be OperSymbol of S st
       [o,the carrier of S] = e.{} & the_result_sort_of o=ar/.b by A6;
     thus thesis by A7;
    end;
   then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
     f = x by A2;
   hence thesis;
 end;

theorem Th9:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S,
    p be 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 be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n)
  proof
   let S be non void non empty ManySortedSign,
       X be non-empty ManySortedSet of the carrier of S,
       o be OperSymbol of S,
       p be FinSequence of TS(DTConMSA(X));
   set AR = the Arity of S,
      cr = the carrier of S,
      ar = the_arity_of o;
   thus p in ((FreeSort X)# * AR).o implies
    dom p = dom (the_arity_of o) &
    for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n)
    proof
     assume A1: p in ((FreeSort X)# * (the Arity of S)).o;
       AR.o = ar by MSUALG_1:def 6;
     then p in product ((FreeSort X) * ar) by A1,Th1;
     then A2: dom p = dom ((FreeSort X) * ar) &
     for x be set st x in dom ((FreeSort X) * ar)
              holds p.x in ((FreeSort X) * ar).x by CARD_3:18;
     A3: rng ar c= cr by FINSEQ_1:def 4;
     A4: dom ((FreeSort X)) = cr by PBOOLE:def 3;
     then A5: dom ((FreeSort X) * ar) = dom ar by A3,RELAT_1:46;
     thus dom p = dom ar by A2,A3,A4,RELAT_1:46;
     let n be Nat;
     assume A6: n in dom p;
     then ((FreeSort X) * ar).n = (FreeSort X).(ar.n) by A2,FUNCT_1:22
        .= (FreeSort X). (ar/.n) by A2,A5,A6,FINSEQ_4:def 4
        .= FreeSort(X,ar/.n) by Def13;
     hence thesis by A2,A6;
    end;
   assume A7: dom p = dom (the_arity_of o) &
   for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n);
     AR.o = ar by MSUALG_1:def 6;
   then A8: ((FreeSort X)# * AR).o = product ((FreeSort X) * ar) by Th1;
   A9: rng ar c= cr by FINSEQ_1:def 4;
     dom ((FreeSort X)) = cr by PBOOLE:def 3;
   then A10: dom p = dom ((FreeSort X) * ar) by A7,A9,RELAT_1:46;
     for x be set st x in dom((FreeSort X) * ar) holds p.x in
 ((FreeSort X) * ar).x
    proof
     let x be set;
     assume A11: x in dom ((FreeSort X) * ar);
     then reconsider n = x as Nat by A10;
       FreeSort(X,ar/.n) = (FreeSort X). (ar/.n) by Def13
     .= (FreeSort X).(ar.n) by A7,A10,A11,FINSEQ_4:def 4
     .= ((FreeSort X) * ar).x by A11,FUNCT_1:22;
     hence thesis by A7,A10,A11;
    end;
   hence thesis by A8,A10,CARD_3:18;
  end;

theorem Th10:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S,
    p be 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 void non empty ManySortedSign,
       X be non-empty ManySortedSet of the carrier of S,
       o be OperSymbol of S,
       p be FinSequence of TS(DTConMSA(X));
   set D = DTConMSA(X),
       ar = the_arity_of o;
   A1: Union (coprod X) misses [:the OperSymbols of S,{the carrier of S}:]
        by Th4;
   A2: Sym(o,X) = [o,the carrier of S] by Def11;
   A3: D = DTConstrStr (#
   [:the OperSymbols of S,{the carrier of S}:] \/
     Union (coprod (X qua ManySortedSet of the carrier of S)), REL(X) #) &
   (Terminals (DTConMSA(X))) = Union (coprod X) &
   NonTerminals(DTConMSA(X)) = [:the OperSymbols of S,{the carrier of S}:]
      by Def10,Th6;
   thus Sym(o,X) ==> roots p implies p in ((FreeSort X)# * (the Arity of S)).o
    proof
     assume Sym(o,X) ==> roots p;
     then A4: [[o,the carrier of S],roots p] in REL(X) by A2,A3,LANG1:def 1;
     then reconsider r = roots p as
      Element of
        ([:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X))*
                                                          by ZFMISC_1:106;
     A5: len r = len ar &
     for x be set st x in dom r holds
       (r.x in [:the OperSymbols of S,{the carrier of S}:] implies
      for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds
                     the_result_sort_of o1 = ar.x) &
       (r.x in Union (coprod X) implies r.x in coprod(ar.x,X)) by A4,Th5;
     A6: dom p = dom r by DTCONSTR:def 1;
     A7: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
       for n be Nat st n in dom p holds p.n in FreeSort(X,ar/.n)
      proof let n be Nat;
      set s = ar/.n,
          A = {a where a is Element of TS D:
              (ex x be set st x in X.s & a = root-tree [x,s]) or
              ex o be OperSymbol of S st
                 [o,the carrier of S] = a.{} & the_result_sort_of o = s};
       A8: A = FreeSort(X,s) by Def12;
       assume A9: n in dom p;
       then consider T be DecoratedTree such that
       A10: T = p.n & r.n = T.{} by DTCONSTR:def 1;
       A11: rng r c=
          [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
             by FINSEQ_1:def 4;
       A12: r.n in rng r by A6,A9,FUNCT_1:def 5;
       A13: rng p c= TS D by FINSEQ_1:def 4;
         p.n in rng p by A9,FUNCT_1:def 5;
       then reconsider T as Element of TS(D) by A10,A13;
       per cases by A11,A12,XBOOLE_0:def 2;
       suppose
A14:      r.n in [:the OperSymbols of S,{the carrier of S}:];
        then consider o1 being OperSymbol of S,
                 x2 being Element of {the carrier of S} such that
A15:       r.n = [o1,x2] by DOMAIN_1:9;
A16:      x2 = the carrier of S by TARSKI:def 1;
        then the_result_sort_of o1 = ar.n by A4,A6,A9,A14,A15,Th5
         .= ar/.n by A5,A6,A7,A9,FINSEQ_4:def 4;
        then (ex x be set st x in X.s & T = root-tree [x,s]) or
         ex o be OperSymbol of S
             st [o,the carrier of S] = T.{} & the_result_sort_of o = s
          by A10,A15,A16;
        hence thesis by A8,A10;
       suppose A17: r.n in Union (coprod X);
        then r.n in coprod(ar.n,X) by A4,A6,A9,Th5;
        then r.n in coprod(s,X) by A5,A6,A7,A9,FINSEQ_4:def 4;
        then consider a be set such that
        A18: a in X.s & r.n = [a,s] by Def2;
        reconsider t = r.n as Terminal of D by A17,Th6;
          T = root-tree t by A10,DTCONSTR:9;
        hence thesis by A8,A10,A18;
      end;
     hence thesis by A5,A6,A7,Th9;
    end;
   set r = roots p,
       OU = [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X);
   assume A19: p in ((FreeSort X)# * (the Arity of S)).o;
   then A20: dom p = dom ar &
   for n be Nat st n in dom p holds p.n in FreeSort(X,ar/.n) by Th9;
   A21: dom p = dom r by DTCONSTR:def 1;
   A22: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
     rng r c= [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
    proof
     let x be set;
     assume x in rng r;
     then consider n be set such that
     A23: n in dom r & r.n = x by FUNCT_1:def 5;
     reconsider n as Nat by A23;
     set s = ar/.n,
         A = {a where a is Element of TS D:
              (ex x be set st x in X.s & a = root-tree [x,s]) or
                ex o be OperSymbol of S st [o,the carrier of S] = a.{}
                 & the_result_sort_of o = s};
     A24: A = FreeSort(X,s) by Def12;
       p.n in FreeSort(X,s) by A19,A21,A23,Th9;
     then consider a be Element of TS D such that
     A25: a = p.n and
     A26: (ex x be set st x in X.s & a = root-tree [x,s]) or
         ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
             the_result_sort_of o = s by A24;
     consider T be DecoratedTree such that
     A27: T = p.n & r.n = T.{} by A21,A23,DTCONSTR:def 1;
     per cases by A26;
     suppose ex x be set st x in X.s & a = root-tree [x,s];
      then consider y be set such that
      A28: y in X.s & a = root-tree [y,s];
      A29: a.{} = [y,s] by A28,TREES_4:3;
      A30: [y,s] in coprod(s,X) by A28,Def2;
        dom coprod(X) = the carrier of S by PBOOLE:def 3;
      then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5;
      then coprod(s,X) in rng coprod(X) by Def3;
      then [y,s] in union rng coprod(X) by A30,TARSKI:def 4;
      then [y,s] in Union (coprod X) by PROB_1:def 3;
      hence thesis by A23,A25,A27,A29,XBOOLE_0:def 2;
     suppose ex o be OperSymbol of S st [o,the carrier of S] = a.{}
            & the_result_sort_of o = s;
      then consider o1 be OperSymbol of S such that
      A31: [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s;
        the carrier of S in {the carrier of S} by TARSKI:def 1;
      then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of S}
:]
                     by ZFMISC_1:106;
      hence thesis by A23,A25,A27,A31,XBOOLE_0:def 2;
    end;
   then reconsider r as FinSequence of OU by FINSEQ_1:def 4;
   reconsider r as Element of OU* by FINSEQ_1:def 11;
   A32: len r = len ar by A20,A21,A22,FINSEQ_1:8;
     for x be set st x in dom r holds
    (r.x in [:the OperSymbols of S,{the carrier of S}:] implies
     for o1 be OperSymbol of S st [o1,the carrier of S] = r.x
     holds the_result_sort_of o1 = ar.x) &
    (r.x in Union (coprod X) implies r.x in coprod(ar.x,X))
     proof
      let x be set;
      assume A33: x in dom r;
      then reconsider n = x as Nat;
      set s = ar/.n,
          A = {a where a is Element of TS D:
              (ex x be set st x in X.s & a = root-tree [x,s]) or
              ex o be OperSymbol of S st
                 [o,the carrier of S] = a.{} & the_result_sort_of o = s};
      A34: A = FreeSort(X,s) by Def12;
        p.n in FreeSort(X,s) by A19,A21,A33,Th9;
      then consider a be Element of TS D such that
      A35: a = p.n and
      A36: (ex x be set st x in X.s & a = root-tree [x,s]) or
         ex o be OperSymbol of S st [o,the carrier of S] = a.{}
               & the_result_sort_of o = s by A34;
      consider T be DecoratedTree such that
      A37: T = p.n & r.n = T.{} by A21,A33,DTCONSTR:def 1;
      A38: s = ar.n by A20,A21,A33,FINSEQ_4:def 4;
      thus r.x in [:the OperSymbols of S,{the carrier of S}:] implies
       for o1 be OperSymbol of S st [o1,the carrier of S] = r.x holds
        the_result_sort_of o1 = ar.x
       proof
        assume A39: r.x in [:the OperSymbols of S,{the carrier of S}:];
        let o1 be OperSymbol of S;
        assume A40: [o1,the carrier of S] = r.x;
           now given y be set such that
          A41: y in X.s & a = root-tree [y,s];
          A42: r.x = [y,s] by A35,A37,A41,TREES_4:3;
          A43: [y,s] in coprod(s,X) by A41,Def2;
            dom coprod(X) = the carrier of S by PBOOLE:def 3;
          then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5;
          then coprod(s,X) in rng coprod(X) by Def3;
          then r.x in union rng coprod(X) by A42,A43,TARSKI:def 4;
          then r.x in Union (coprod X) by PROB_1:def 3;
          hence contradiction by A1,A39,XBOOLE_0:3;
         end;
        then consider o2 be OperSymbol of S such that
        A44: [o2,the carrier of S] = a.{} & the_result_sort_of o2 = s by A36;
         thus thesis by A35,A37,A38,A40,A44,ZFMISC_1:33;
       end;
      assume A45: r.x in Union (coprod X);
         now given o1 be OperSymbol of S such that
        A46: [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s;
           the carrier of S in {the carrier of S} by TARSKI:def 1;
         then [o1,the carrier of S] in [:the OperSymbols of S,{the carrier of
S}:]
                 by ZFMISC_1:106;
        hence contradiction by A1,A35,A37,A45,A46,XBOOLE_0:3;
       end;
      then consider y be set such that
      A47: y in X.s & a = root-tree [y,s] by A36;
        r.x = [y,s] by A35,A37,A47,TREES_4:3;
      hence thesis by A38,A47,Def2;
     end;
   then [[o,the carrier of S],r] in REL X by A32,Th5;
   hence thesis by A2,A3,LANG1:def 1;
  end;

canceled;

theorem Th12:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S holds
 union rng (FreeSort X) = TS (DTConMSA(X))
  proof
   let S be non void non empty ManySortedSign,
       X be non-empty ManySortedSet of the carrier of S;
   set D = DTConMSA(X);
   A1: dom (FreeSort X) = the carrier of S &
       dom (coprod X) = the carrier of S by PBOOLE:def 3;
   thus union rng (FreeSort X) c= TS D
    proof
     let x; assume x in union rng (FreeSort X);
     then consider A be set such that
     A2: x in A & A in rng (FreeSort X) by TARSKI:def 4;
     consider s be set such that
     A3: s in dom (FreeSort X) & (FreeSort X).s = A by A2,FUNCT_1:def 5;
     reconsider s as SortSymbol of S by A3,PBOOLE:def 3;
       A = FreeSort(X,s) by A3,Def13
      .= {a where a is Element of TS(D):
          (ex x be set st x in X.s & a = root-tree [x,s]) or
          ex o1 be OperSymbol of S st
              [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s}
                                          by Def12;
     then consider a be Element of TS(D) such that
     A4: a = x and
        (ex x be set st x in X.s & a = root-tree [x,s]) or
       ex o1 be OperSymbol of S st
         [o1,the carrier of S]=a.{} & the_result_sort_of o1 = s by A2;
     thus thesis by A4;
    end;
   let x;
   assume x in TS D;
   then reconsider t = x as Element of TS(D);
   A5: rng t c= the carrier of D by TREES_2:def 9;
     {} in dom t by TREES_1:47;
   then A6: t.{} in rng t by FUNCT_1:def 5;
   A7: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
   A8: Terminals D = Union (coprod X) &
       NonTerminals D = [:the OperSymbols of S,{the carrier of S}:] by Th6;
   per cases by A5,A6,A7,XBOOLE_0:def 2;
   suppose A9: t.{} in Terminals D;
    then reconsider a = t.{} as Terminal of D;
    A10: t = root-tree a by DTCONSTR:9;
      a in union rng(coprod X) by A8,A9,PROB_1:def 3;
    then consider A be set such that
    A11: a in A & A in rng(coprod X) by TARSKI:def 4;
    consider s be set such that
    A12: s in dom(coprod X) & (coprod X).s = A by A11,FUNCT_1:def 5;
    reconsider s as SortSymbol of S by A12,PBOOLE:def 3;
      A = coprod(s,X) by A12,Def3;
    then consider b be set such that
    A13: b in X.s & a = [b,s] by A11,Def2; t in
 {aa where aa is Element of TS(D):
         (ex x be set st x in X.s & aa = root-tree [x,s]) or
      ex o1 be OperSymbol of S st
       [o1,the carrier of S] =aa.{} & the_result_sort_of o1 = s} by A10,A13
;
    then t in FreeSort(X,s) by Def12;
    then A14: t in (FreeSort X).s by Def13;
      (FreeSort X).s in rng (FreeSort X) by A1,FUNCT_1:def 5;
    hence thesis by A14,TARSKI:def 4;
   suppose t.{} in NonTerminals D;
    then reconsider a = t.{} as NonTerminal of D;
    consider o being OperSymbol of S,
                  x2 being Element of {the carrier of S} such that
A15:  a = [o,x2] by A8,DOMAIN_1:9;
A16:  x2 = the carrier of S by TARSKI:def 1;
    set rs = the_result_sort_of o;
      t in {aa where aa is Element of TS(D):
         (ex x be set st x in X.rs & aa = root-tree [x,rs]) or
      ex o1 be OperSymbol of S st
            [o1,the carrier of S] =aa.{} & the_result_sort_of o1 = rs}
                   by A15,A16;
    then t in FreeSort(X,rs) by Def12;
    then A17: t in (FreeSort X).rs by Def13;
      (FreeSort X).rs in rng (FreeSort X) by A1,FUNCT_1:def 5;
    hence thesis by A17,TARSKI:def 4;
  end;

theorem Th13:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S
 st s1 <> s2 holds (FreeSort X).s1 misses (FreeSort X).s2
  proof
   let S be non void non empty ManySortedSign,
       X be non-empty ManySortedSet of the carrier of S,
       s1,s2 be SortSymbol of S;
   assume that A1: s1 <> s2 and
   A2: (FreeSort X).s1 /\ (FreeSort X).s2 <> {};
   consider x such that
   A3: x in (FreeSort X).s1 /\ (FreeSort X).s2 by A2,XBOOLE_0:def 1;
   A4: x in (FreeSort X).s1 & x in (FreeSort X).s2 by A3,XBOOLE_0:def 3;
   A5: (FreeSort X).s1 = FreeSort(X,s1) &
       (FreeSort X).s2 = FreeSort(X,s2) by Def13;
   set D = DTConMSA(X),
       A1 = {a where a is Element of TS(D):
        (ex x be set st x in X.s1 & a = root-tree [x,s1]) or
        ex o1 be OperSymbol of S st
               [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1},
       A2 = {a where a is Element of TS(D):
        (ex x be set st x in X.s2 & a = root-tree [x,s2]) or
        ex o1 be OperSymbol of S st
               [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s2};
   A6: A1 = (FreeSort X).s1 & A2 = (FreeSort X).s2 by A5,Def12;
   then consider a be Element of TS D such that
   A7: a = x and
   A8: (ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1]) or
        ex o1 be OperSymbol of S st
          [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1 by A4;
   consider b be Element of TS D such that
   A9: b = x and
   A10: (ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]) or
   ex o2 be OperSymbol of S st
       [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2 by A4,A6;
   per cases by A8;
    suppose ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1];
    then consider x1 be set such that
    A11: x1 in X.s1 & a = root-tree [x1,s1];
       now per cases by A10;
     case ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
      then consider x2 be set such that
      A12: x2 in X.s2 & b = root-tree [x2,s2];
        [x1,s1] = [x2,s2] by A7,A9,A11,A12,TREES_4:4;
      hence contradiction by A1,ZFMISC_1:33;
     case ex o2 be OperSymbol of S st
       [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2;
      then consider o2 be OperSymbol of S such that
      A13: [o2,the carrier of S] = b.{} & the_result_sort_of o2 = s2;
         [o2,the carrier of S] = [x1,s1] by A7,A9,A11,A13,TREES_4:3;
      then A14:the carrier of S = s1 by ZFMISC_1:33;
        for X be set holds not X in X;
      hence contradiction by A14;
     end;
    hence contradiction;
    suppose
      ex o1 be OperSymbol of S st
       [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1;
    then consider o1 be OperSymbol of S such that
    A15: [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1;
       now per cases by A10;
     case ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
      then consider x2 be set such that
      A16: x2 in X.s2 & b = root-tree [x2,s2];
         [o1,the carrier of S] = [x2,s2] by A7,A9,A15,A16,TREES_4:3;
      then A17: the carrier of S = s2 by ZFMISC_1:33;
        for X be set holds not X in X;
      hence contradiction by A17;
     case ex o2 be OperSymbol of S st
       [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2;
      then consider o2 be OperSymbol of S such that
      A18: [o2,the carrier of S] = b.{} & the_result_sort_of o2 = s2;
      thus contradiction by A1,A7,A9,A15,A18,ZFMISC_1:33;
     end;
    hence contradiction;
  end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     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 :Def14:
for p be FinSequence of TS(DTConMSA(X)) st Sym(o,X) ==> roots p holds
  it.p = (Sym(o,X))-tree p;
 existence
  proof
   set AL = ((FreeSort X)# * (the Arity of S)).o,
       AX = ((FreeSort X) * (the ResultSort of S)).o,
       D = DTConMSA(X),
       O = the OperSymbols of S,
       rs = the_result_sort_of o,
       RS = the ResultSort of S;
   defpred P[set,set] means
   for p be FinSequence of TS D st p = $1 holds $2 = (Sym(o,X))-tree p;

   A1: for x be set st x in AL ex y be set st y in AX & P[x,y]
    proof
     let x be set;
     assume A2: x in AL;
     then reconsider p = x as FinSequence of TS(D) by Th8;
     take y = (Sym(o,X))-tree p;
        o in O;
     then o in dom ((FreeSort X) * RS) by PBOOLE:def 3;
     then A3: AX =(FreeSort X).(RS.o) by FUNCT_1:22
      .= (FreeSort X).rs by MSUALG_1:def 7
      .= FreeSort(X,rs) by Def13;
     set A = {a where a is Element of TS(D):
       (ex x be set st x in X.rs & a = root-tree [x,rs]) or
       ex o1 be OperSymbol of S st
          [o1,the carrier of S] = a.{} & the_result_sort_of o1 = rs};
     A4: A = AX by A3,Def12;
       Sym(o,X) ==> roots p by A2,Th10;
     then reconsider a = (Sym(o,X))-tree p as Element of TS D by DTCONSTR:def 4
;
       (ex q being DTree-yielding FinSequence st p = q & dom a = tree doms q) &
      a.{} = Sym(o,X) & for n be Nat st n < len p holds a|<*n*> = p.(n+1)
                                            by TREES_4:def 4;
     then consider q being DTree-yielding FinSequence such that
     A5: p = q & dom a = tree doms q &
     a.{} = Sym(o,X) &
     for n be Nat st n < len p holds a|<*n*> = p.(n+1);
       Sym(o,X) = [o,the carrier of S] by Def11;
     hence y in AX by A4,A5;
     thus P[x,y];
    end;
   consider f be Function such that
   A6: dom f = AL & rng f c= AX &
       for x be set st x in AL holds P[x,f.x] from NonUniqBoundFuncEx(A1);
   reconsider g = f as Function of AL,rng f by A6,FUNCT_2:3;
   reconsider g as Function of AL,AX by A6,FUNCT_2:4;
   take g;
   let p be FinSequence of TS D;
   assume Sym(o,X) ==> roots p;
   then p in AL by Th10;
   hence thesis by A6;
  end;
 uniqueness
  proof
   set AL = ((FreeSort X)# * (the Arity of S)).o,
       AX = ((FreeSort X) * (the ResultSort of S)).o,
       D = DTConMSA(X);
   let f,g be Function of AL, AX; assume that
   A7: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds
          f.p = (Sym(o,X))-tree p and
   A8: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds
          g.p = (Sym(o,X))-tree p;
   A9: dom f = AL & dom g = AL by FUNCT_2:def 1;
     for x be set st x in AL holds f.x = g.x
    proof
     let x be set;
     assume A10: x in AL;
     then reconsider p = x as FinSequence of TS(D) by Th8;
       Sym(o,X) ==> roots p by A10,Th10;
     then f.p = (Sym(o,X))-tree p & g.p = (Sym(o,X))-tree p by A7,A8;
     hence thesis;
    end;
   hence thesis by A9,FUNCT_1:9;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
func FreeOper(X) -> ManySortedFunction of (FreeSort X)# * (the Arity of S),
              (FreeSort X) * (the ResultSort of S) means :Def15:
for o be OperSymbol of S holds it.o = DenOp(o,X);
 existence
  proof
   set Y = the OperSymbols of S;
   defpred P[set,set] means
   for o be OperSymbol of S st $1 = o holds $2 = DenOp(o,X);
   A1: for x be set st x in Y ex y be set st P[x,y]
    proof
     let x be set;
     assume x in Y;
     then reconsider o = x as OperSymbol of S;
     take DenOp(o,X);
     thus thesis;
    end;
   consider f be Function such that
   A2: dom f = Y & for x be set st x in
 Y holds P[x,f.x] from NonUniqFuncEx(A1);
   reconsider f as ManySortedSet of Y by A2,PBOOLE:def 3;
     for x be set st x in dom f holds f.x is Function
    proof
     let x be set;
     assume x in dom f;
     then reconsider o = x as OperSymbol of S by A2;
       f.o = DenOp(o,X) by A2;
     hence thesis;
    end;
   then reconsider f as ManySortedFunction of Y by PRALG_1:def 15;
     for x be set st x in Y 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;
     assume x in Y;
     then reconsider o = x as OperSymbol of S;
       f.o = DenOp(o,X) by A2;
     hence thesis;
    end;
   then reconsider f as ManySortedFunction of (FreeSort X)# * (the Arity of S),
     (FreeSort X) * (the ResultSort of S) by MSUALG_1:def 2;
   take f;
   let o be OperSymbol of S;
   thus thesis by A2;
  end;
 uniqueness
  proof
   let A,B be ManySortedFunction of
           (FreeSort X)# * (the Arity of S),
           (FreeSort X) * (the ResultSort of S);
   assume that A3: for o be OperSymbol of S holds A.o = DenOp(o,X) and
           A4: for o be OperSymbol of S holds B.o = DenOp(o,X);
     for i be set st i in the OperSymbols of S holds A.i = B.i
    proof
     let i be set;
     assume i in the OperSymbols of S;
     then reconsider s = i as OperSymbol of S;
       A.s = DenOp(s,X) & B.s = DenOp(s,X) by A3,A4;
     hence thesis;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

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

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
cluster FreeMSA(X) -> strict non-empty;
 coherence
  proof
   MSAlgebra (# FreeSort(X), FreeOper(X) #) = FreeMSA X by Def16;
    hence thesis by MSUALG_1:def 8;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     s be SortSymbol of S;
func FreeGen(s,X) -> Subset of (FreeSort(X)).s means :Def17:
for x be set holds
     x in it iff ex a be set st a in X.s & x = root-tree [a,s];
 existence
  proof
   set D = DTConMSA(X);
   defpred P[set] means ex a be set st a in X.s & $1 = root-tree [a,s];
   consider A be set such that
   A1: for x holds x in A iff x in (FreeSort(X)).s & P[x] from Separation;
     A c= (FreeSort(X)).s
    proof
     let x;
     assume x in A;
     hence thesis by A1;
    end;
   then reconsider A as Subset of (FreeSort(X)).s;
      for x holds x in A iff P[x]
    proof
     let x;
     thus x in A implies P[x] by A1;
     assume A2: P[x];
     then consider a be set such that
     A3: a in X.s & x = root-tree [a,s];
     A4: (FreeSort X).s = FreeSort(X,s) by Def13;
     set A = {aa where aa is Element of TS(D):
       (ex x be set st x in X.s & aa = root-tree [x,s]) or
       ex o1 be OperSymbol of S st
           [o1,the carrier of S] = aa.{} & the_result_sort_of o1 = s};
     A5: A = (FreeSort X).s by A4,Def12;
     set sa = [a,s];
     A6: sa in coprod(s,X) by A3,Def2;
     A7: Terminals D = Union (coprod X) by Th6;
       dom coprod(X) = the carrier of S by PBOOLE:def 3;
     then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 5;
     then coprod(s,X) in rng coprod(X) by Def3;
     then sa in union rng coprod(X) by A6,TARSKI:def 4;
     then A8: sa in Terminals D by A7,PROB_1:def 3;
     then reconsider sa as Symbol of D;
     reconsider b = root-tree sa as Element of TS(D) by A8,DTCONSTR:def 4;
       b in A & b = x by A3;
     hence thesis by A1,A2,A5;
    end;
    hence thesis;
  end;
 uniqueness
  proof
   let A,B be Subset of (FreeSort(X)).s; assume that
   A9: for x be set holds
           x in A iff ex a be set st a in X.s & x = root-tree [a,s] and
   A10: for x be set holds
           x in B iff ex a be set st a in X.s & x = root-tree [a,s];
   thus A c= B
    proof
     let x be set;
     assume x in A;
     then ex a be set st a in X.s & x = root-tree [a,s] by A9;
     hence thesis by A10;
    end;
   let x be set;
   assume x in B;
   then ex a be set st a in X.s & x = root-tree [a,s] by A10;
   hence thesis by A9;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     s be SortSymbol of S;
cluster FreeGen(s,X) -> non empty;
 coherence
  proof
   consider x such that
   A1: x in X.s by XBOOLE_0:def 1;
    ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1;
   hence thesis by Def17;
  end;
end;

theorem Th14:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S,
    s be 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 void non empty ManySortedSign,
      X be non-empty ManySortedSet of the carrier of S,
      s be SortSymbol of S;
  set D = DTConMSA(X),
      A = {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s};
  thus FreeGen(s,X) c= A
   proof
    let x be set;
    assume x in FreeGen(s,X);
    then consider a be set such that
    A1: a in X.s & x = root-tree [a,s] by Def17;
    A2: [a,s] in Terminals D by A1,Th7;
    then reconsider t = [a,s] as Symbol of D;
      t`2 = s by MCART_1:7;
    hence thesis by A1,A2;
   end;
  let x be set;
  assume x in A;
  then consider t be Symbol of D such that
  A3: x = root-tree t & t in Terminals D & t`2 = s;
  consider s1 be SortSymbol of S, a be set such that
  A4: a in X.s1 & t = [a,s1] by A3,Th7;
    s = s1 by A3,A4,MCART_1:7;
  hence thesis by A3,A4,Def17;
 end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
func FreeGen(X) -> GeneratorSet of FreeMSA(X) means :Def18:
for s be SortSymbol of S holds it.s = FreeGen(s,X);
 existence
  proof
   set FM = FreeMSA(X),
       D = DTConMSA(X);
   A1: FM = MSAlgebra (# FreeSort(X), FreeOper(X) #) by Def16;
   deffunc F(Element of S)=FreeGen($1,X);
   consider f be Function such that
   A2: dom f = the carrier of S &
       for s be Element of S holds f.s = F(s)
        from LambdaB;
   reconsider f as ManySortedSet of the carrier of S by A2,PBOOLE:def 3;
     f c= the Sorts of FM
    proof
     let x;
     assume x in the carrier of S;
     then reconsider s = x as SortSymbol of S;
       f.s = FreeGen(s,X) & FreeGen(s,X) c= (FreeSort X).s by A2;
     hence thesis by A1;
    end;
   then reconsider f as MSSubset of FM by MSUALG_2:def 1;
     the Sorts of GenMSAlg(f) = the Sorts of FM
    proof
       the Sorts of GenMSAlg(f) is MSSubset of FM by MSUALG_2:def 10;
     hence A3: the Sorts of GenMSAlg(f) c= the Sorts of FM by MSUALG_2:def 1;
     defpred P[set] means
     $1 in union rng (the Sorts of GenMSAlg(f));
     A4: for s be Symbol of D st s in Terminals D holds P[root-tree s]
      proof
       let t be Symbol of D;
       assume t in Terminals D;
       then t in Union (coprod X) by Th6;
       then t in union rng(coprod X) by PROB_1:def 3;
       then consider A be set such that
       A5: t in A & A in rng (coprod X) by TARSKI:def 4;
       consider s be set such that
       A6: s in dom (coprod X) & (coprod X).s = A by A5,FUNCT_1:def 5;
       reconsider s as SortSymbol of S by A6,PBOOLE:def 3;
         A = coprod(s,X) by A6,Def3;
       then consider a be set such that
       A7: a in X.s & t = [a,s] by A5,Def2;
         f is MSSubset of GenMSAlg(f) by MSUALG_2:def 18;
       then f c= the Sorts of GenMSAlg(f) by MSUALG_2:def 1;
       then f.s c= (the Sorts of GenMSAlg(f)).s by PBOOLE:def 5;
       then A8: FreeGen(s,X) c= (the Sorts of GenMSAlg(f)).s by A2;
       A9: root-tree t in FreeGen(s,X) by A7,Def17;
         dom (the Sorts of GenMSAlg(f)) = the carrier of S by PBOOLE:def 3;
       then (the Sorts of GenMSAlg(f)).s in rng (the Sorts of GenMSAlg(f))
                                          by FUNCT_1:def 5;
       hence thesis by A8,A9,TARSKI:def 4;
      end;
     A10: for nt being Symbol of D, ts being FinSequence of TS(D)
        st nt ==> roots ts &
         for t being DecoratedTree of the carrier of D st t in
 rng ts holds P[t]
      holds P[nt-tree ts]
       proof
        let nt be Symbol of D, ts be FinSequence of TS(D);
        assume A11: nt ==> roots ts &
        for t being DecoratedTree of the carrier of D st t in
 rng ts holds P[t];
        set G = GenMSAlg(f),
         OU = [:the OperSymbols of S,{the carrier of S}:] \/
              Union (coprod (X qua ManySortedSet of the carrier of S));
        reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 10;
        set AR = the Arity of S,
            RS = the ResultSort of S,
            BH = B# * the Arity of S,
            O = the OperSymbols of S;
        A12: B is opers_closed by MSUALG_2:def 10;
        A13: [nt,roots ts] in the Rules of D by A11,LANG1:def 1;
        A14: D = DTConstrStr (# OU, REL(X)#) & Terminals D = Union (coprod X)
         by Def10,Th6;
        then A15: [nt,roots ts] in REL(X) by A11,LANG1:def 1;
        reconsider sy = nt as Element of OU by A14;
        reconsider rt = roots ts as Element of OU* by A13,A14,ZFMISC_1:106;
          [sy,rt] in REL(X) by A11,A14,LANG1:def 1;
        then sy in [:the OperSymbols of S,{the carrier of S}:] by Def9;
        then consider o being OperSymbol of S,
                      x2 being Element of {the carrier of S} such that
A16:      sy = [o,x2] by DOMAIN_1:9;
A17:      x2 = the carrier of S by TARSKI:def 1;
        set ar = the_arity_of o,
            rs = the_result_sort_of o;
          B is_closed_on o by A12,MSUALG_2:def 7;
        then A18: rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 6;
        A19: Sym(o,X) = [o,the carrier of S] & nt = [o,the carrier of S]
                  by A16,Def11,TARSKI:def 1;
        A20: Den(o,FM) = (FreeOper X).o by A1,MSUALG_1:def 11
        .= DenOp(o,X) by Def15;
        A21: dom (FreeSort X) = the carrier of S & o in O &
            dom B = the carrier of S & dom RS = O &
            rng RS c= the carrier of S & AR.o = ar & RS.o = rs
            by FUNCT_2:def 1,MSUALG_1:def 6,def 7,PBOOLE:def 3,RELSET_1:12;
          dom DenOp(o,X) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
        then A22: ts in dom DenOp(o,X) by A11,A19,Th10;
        A23: BH.o = product (B * ar) by A21,Th1;
          rng ar c= the carrier of S by FINSEQ_1:def 4;
        then A24: dom (B * ar) = dom ar by A21,RELAT_1:46;
        A25: dom (roots ts) = dom ts by DTCONSTR:def 1;
        A26: len rt = len ar &
        for x st x in dom rt holds
         (rt.x in [:the OperSymbols of S,{the carrier of S}:] implies
         for o1 be OperSymbol of S st [o1,the carrier of S] = rt.x holds
                     the_result_sort_of o1 = ar.x) &
         (rt.x in Union (coprod X) implies rt.x in coprod(ar.x,X))
                            by A15,A16,A17,Th5;
        A27: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3;
        then A28: dom ts = dom ar by A13,A14,A16,A17,A25,Th5;
          for x st x in dom (B * ar) holds ts.x in (B * ar).x
         proof
          let x;
          assume A29: x in dom (B * ar);
          then reconsider n = x as Nat by A24;
          A30: rng ts c= TS D by FINSEQ_1:def 4;
          A31: ts.n in rng ts by A24,A25,A26,A27,A29,FUNCT_1:def 5;
          then reconsider T = ts.x as Element of TS(D) by A30;
            P[T] by A11,A31;
          then consider A be set such that
          A32: T in A & A in rng (the Sorts of G) by TARSKI:def 4;
          consider s be set such that
          A33: s in dom(the Sorts of G) & (the Sorts of G).s = A
                                                        by A32,FUNCT_1:def 5;
          reconsider s as SortSymbol of S by A33,PBOOLE:def 3;
          A34: (B * ar).x = B.(ar.n) by A29,FUNCT_1:22
          .= B.(ar/.n) by A24,A29,FINSEQ_4:def 4;
          set b = ar/.n,
              A1 = {a where a is Element of TS D:
                  (ex x be set st x in X.b & a = root-tree [x,b]) or
              ex o be OperSymbol of S st
                 [o,the carrier of S] = a.{} & the_result_sort_of o = b};
          A35: A1 = FreeSort(X,b) by Def12
               .= (FreeSort X).b by Def13;
          consider t be DecoratedTree such that
          A36: t = ts.n & rt.n = t.{} by A24,A25,A26,A27,A29,DTCONSTR:def 1;
          A37: rng rt c=
                [:the OperSymbols of S,{the carrier of S}:] \/ Union (coprod X)
            by FINSEQ_1:def 4;
          A38: rt.n in rng rt by A24,A26,A27,A29,FUNCT_1:def 5;
          A39: now per cases by A37,A38,XBOOLE_0:def 2;
           suppose
A40:          rt.n in [:the OperSymbols of S,{the carrier of S}:];
            then consider o1 being OperSymbol of S,
                     x2 being Element of {the carrier of S} such that
A41:           rt.n = [o1,x2] by DOMAIN_1:9;
A42:          x2 = the carrier of S by TARSKI:def 1;
            then the_result_sort_of o1 = ar.n by A13,A14,A16,A17,A24,A25,A28,
A29,A40,A41,Th5
              .= b by A24,A29,FINSEQ_4:def 4;
            hence T in (FreeSort X).b by A35,A36,A41,A42;
           suppose A43: rt.n in Union (coprod X);
            then rt.n in coprod(ar.n,X) by A13,A14,A16,A17,A24,A25,A28,A29,Th5
;
            then rt.n in coprod(b,X) by A24,A29,FINSEQ_4:def 4;
            then consider a be set such that
            A44: a in X.b & rt.n = [a,b] by Def2;
            reconsider tt = rt.n as Terminal of D by A43,Th6;
              T = root-tree tt by A36,DTCONSTR:9;
            hence T in (FreeSort X).b by A35,A44;
          end;
             now assume b <> s;
            then A45: (FreeSort X).s misses (FreeSort X).b by Th13;
              (the Sorts of G).s c= (the Sorts of FM).s by A3,PBOOLE:def 5;
            hence contradiction by A1,A32,A33,A39,A45,XBOOLE_0:3;
           end;
          hence thesis by A32,A33,A34;
         end;
        then ts in BH.o by A23,A24,A25,A26,A27,CARD_3:18;
        then ts in (dom DenOp(o,X)) /\ (BH.o) by A22,XBOOLE_0:def 3;
        then A46: ts in dom (DenOp(o,X) | (BH.o)) by FUNCT_1:68;
        then (DenOp(o,X) | (BH.o)).ts = (DenOp(o,X)).ts by FUNCT_1:68
         .= nt-tree ts by A11,A19,Def14;
        then A47: nt-tree ts in rng ((Den(o,FM))|(BH.o)) by A20,A46,FUNCT_1:def
5;
  dom (B * RS) = O by PBOOLE:def 3;
        then (B * RS).o = B.rs & B.rs in rng B by A21,FUNCT_1:22,def 5;
        hence thesis by A18,A47,TARSKI:def 4;
       end;
     A48: for t being DecoratedTree of the carrier of D
            st t in TS D holds P[t] from DTConstrInd(A4,A10);
     A49: union rng(the Sorts of FM) c= union rng (the Sorts of GenMSAlg(f))
      proof
       let x;
       assume x in union rng(the Sorts of FM);
       then consider A be set such that
       A50: x in A & A in rng(the Sorts of FM) by TARSKI:def 4;
       consider s be set such that
       A51: s in dom (FreeSort X) & (FreeSort X).s = A by A1,A50,FUNCT_1:def 5;
       reconsider s as SortSymbol of S by A51,PBOOLE:def 3;
       set D = DTConMSA(X);
         A = FreeSort(X,s) by A51,Def13
        .= {a where a is Element of TS(D):
          (ex x be set st x in X.s & a = root-tree [x,s]) or
          ex o1 be OperSymbol of S st
               [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s}
                                          by Def12;
       then consider a be Element of TS(D) such that
       A52: a = x and
         (ex x be set st x in X.s & a = root-tree [x,s]) or
       ex o1 be OperSymbol of S st
           [o1,the carrier of S]=a.{} & the_result_sort_of o1 = s by A50;
       thus thesis by A48,A52;
      end;
     let x; assume
       x in the carrier of S;
     then reconsider s = x as SortSymbol of S;
       (the Sorts of FM).s c= (the Sorts of GenMSAlg(f)).s
      proof
       let a be set; assume
       A53: a in (the Sorts of FM).s;
         the carrier of S = dom (the Sorts of FM) by PBOOLE:def 3;
       then (the Sorts of FM).s in rng (the Sorts of FM) by FUNCT_1:def 5;
       then a in union rng (the Sorts of FM) by A53,TARSKI:def 4;
       then consider A be set such that
       A54: a in A & A in rng (the Sorts of GenMSAlg(f)) by A49,TARSKI:def 4;
       consider b be set such that
       A55: b in dom (the Sorts of GenMSAlg(f)) &
           (the Sorts of GenMSAlg(f)).b = A by A54,FUNCT_1:def 5;
       reconsider b as SortSymbol of S by A55,PBOOLE:def 3;
          now assume b <> s;
         then (FreeSort X).s misses (FreeSort X).b by Th13;
         then A56: (FreeSort X).s /\ (FreeSort X).b = {} by XBOOLE_0:def 7;
           (the Sorts of GenMSAlg(f)).b c= (the Sorts of FM).b
                                               by A3,PBOOLE:def 5;
         hence contradiction by A1,A53,A54,A55,A56,XBOOLE_0:def 3;
        end;
       hence thesis by A54,A55;
      end;
     hence thesis;
    end;
   then reconsider f as GeneratorSet of FM by Def4;
   take f;
   thus thesis by A2;
  end;
 uniqueness
  proof
   let A,B be GeneratorSet of FreeMSA(X);
   assume that A57: for s be SortSymbol of S holds A.s = FreeGen(s,X) and
          A58: for s be SortSymbol of S holds B.s = FreeGen(s,X);
     for i be set st i in the carrier of S holds A.i = B.i
    proof
     let i be set;
     assume i in the carrier of S;
     then reconsider s = i as SortSymbol of S;
       A.s = FreeGen(s,X) & B.s = FreeGen(s,X) by A57,A58;
     hence thesis;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

theorem
  for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S
holds FreeGen(X)is non-empty
 proof
  let S be non void non empty ManySortedSign,
      X be non-empty ManySortedSet of the carrier of S;
  let x;
  assume x in the carrier of S;
  then reconsider s = x as SortSymbol of S;
    (FreeGen(X)).s = FreeGen(s,X) by Def18;
  hence thesis;
 end;

theorem
  for S be non void non empty ManySortedSign,
     X be non-empty 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 void non empty ManySortedSign,
      X be non-empty ManySortedSet of the carrier of S;
  set D = DTConMSA(X),
      A = union rng FreeGen(X),
      B = {root-tree t where t is Symbol of D : t in Terminals D};
  A1: dom FreeGen(X) = the carrier of S by PBOOLE:def 3;
  thus A c= B
   proof
    let x;
    assume x in A;
    then consider C be set such that
    A2: x in C & C in rng FreeGen(X) by TARSKI:def 4;
    consider s be set such that
    A3: s in dom FreeGen(X) & (FreeGen(X)).s = C by A2,FUNCT_1:def 5;
    reconsider s as SortSymbol of S by A3,PBOOLE:def 3;
      C = FreeGen(s,X) by A3,Def18
     .= {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}
                                                   by Th14;
    then consider t be Symbol of D such that
    A4: x = root-tree t & t in Terminals D & t`2 = s by A2;
    thus thesis by A4;
   end;
  let x;
  assume x in B;
  then consider t be Symbol of D such that
  A5: x = root-tree t & t in Terminals D;
  consider s be SortSymbol of S, a be set such that
  A6: a in X.s & t = [a,s] by A5,Th7;
    t`2 = s by A6,MCART_1:7;
  then x in {root-tree tt where tt is Symbol of D : tt in Terminals D & tt`2 =
s}
                                 by A5;
  then x in FreeGen(s,X) by Th14;
  then A7: x in (FreeGen(X)).s by Def18;
    (FreeGen(X)).s in rng (FreeGen(X)) by A1,FUNCT_1:def 5;
  hence thesis by A7,TARSKI:def 4;
 end;

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

     then consider t be Symbol of D such that
     A10: i = root-tree t & t in Terminals D & t`2 = s;
       A.(root-tree t) = t`1 & B.(root-tree t) = t`1 by A5,A6,A7,A9,A10;
     hence thesis by A10;
    end;
   hence thesis by A8,FUNCT_1:9;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
func Reverse(X) -> ManySortedFunction of FreeGen(X),X means :Def20:
for s be SortSymbol of S holds it.s = Reverse(s,X);
 existence
  proof
   set I = the carrier of S,
      FG = FreeGen(X);
   defpred P[set,set] means
   for s be SortSymbol of S st s = $1 holds $2 = Reverse(s,X);
   A1: for i be set st i in I ex u be set st P[i,u]
   proof
    let i be set;
    assume i in I;
    then reconsider s = i as SortSymbol of S;
    take Reverse(s,X);
    let s1 be SortSymbol of S;
    assume s1 = i;
    hence thesis;
   end;
  consider H be Function such that
  A2: dom H = I & for i be set st i in I holds P[i,H.i] from NonUniqFuncEx(A1);
  reconsider H as ManySortedSet of I by A2,PBOOLE:def 3;
    for x be set st x in dom H holds H.x is Function
    proof
     let i be set;
     assume i in dom H;
     then reconsider s = i as SortSymbol of S by A2;
       H.s = Reverse(s,X) by A2;
     hence thesis;
    end;
  then reconsider H as ManySortedFunction of I by PRALG_1:def 15;
    for i be set st i in I holds H.i is Function of FG.i,X.i
    proof
     let i be set;
     assume i in I;
     then reconsider s = i as SortSymbol of S;
A3:   (FreeGen X).s = FreeGen(s,X) by Def18;
        H.i = Reverse(s,X) by A2;
     hence thesis by A3;
    end;
  then reconsider H as ManySortedFunction of FG,X by MSUALG_1:def 2;
  take H;
  let s be SortSymbol of S;
  thus thesis by A2;
  end;
 uniqueness
  proof
   let A,B be ManySortedFunction of FreeGen(X),X;assume that
   A4: for s be SortSymbol of S holds A.s = Reverse(s,X) and
   A5: for s be SortSymbol of S holds B.s = Reverse(s,X);
     for i be set st i in the carrier of S holds A.i = B.i
    proof
     let i be set;
     assume i in the carrier of S;
     then reconsider s = i as SortSymbol of S;
       A.s = Reverse(s,X) & B.s = Reverse(s,X) by A4,A5;
     hence thesis;
    end;
  hence thesis by PBOOLE:3;
 end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     A be non-empty ManySortedSet of the carrier of S,
     F be ManySortedFunction of FreeGen(X), A,
     t be Symbol of DTConMSA(X);
assume A1: t in Terminals (DTConMSA(X));
func pi(F,A,t) -> Element of Union A means :Def21:
 for f be Function st f = F.(t`2) holds it = f.(root-tree t);
 existence
  proof
   set FG = FreeGen(X),
        D = DTConMSA(X);
   consider s be SortSymbol of S, x be set such that
   A2: x in X.s & t = [x,s] by A1,Th7;
      FG.s = FreeGen(s,X) by Def18;
   then A3: dom (F.s) = FreeGen(s,X) by FUNCT_2:def 1
    .= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s}
                           by Th14;
     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 5;
   A5: rng (F.s) c= A.s by RELSET_1:12;
     dom A = the carrier of S by PBOOLE:def 3;
   then A.s in rng A by FUNCT_1:def 5;
   then (F.s).(root-tree t) in union rng A by A4,A5,TARSKI:def 4;
   then reconsider eu = (F.s).(root-tree t) as Element of Union A by PROB_1:def
3;
   take eu;
   let f be Function;
   assume f = F.(t`2);
   hence thesis by A2,MCART_1:7;
  end;
 uniqueness
  proof
   let a,b be Element of Union A; assume that
   A6: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and
   A7: for f be Function st f = F.(t`2) holds b = f.(root-tree t);
   consider s be SortSymbol of S, x be set such that
   A8: x in X.s & t = [x,s] by A1,Th7;
   reconsider f = F.s as Function;
     f = F.(t`2) by A8,MCART_1:7;
   then a = f.(root-tree t) & b = f.(root-tree t) by A6,A7;
   hence thesis;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S,
     t be Symbol of DTConMSA(X);
assume A1: ex p be FinSequence st t ==> p;
func @(X,t) -> OperSymbol of S means :Def22:
  [it,the carrier of S] = t;
 existence
  proof
   set D = DTConMSA(X),
      OU = [:the OperSymbols of S,{the carrier of S}:] \/
           Union (coprod (X qua ManySortedSet of the carrier of S));
   consider p be FinSequence such that
   A2: t ==> p by A1;
   A3: [t,p] in the Rules of D by A2,LANG1:def 1;
   A4: D = DTConstrStr (# OU, REL(X) #) by Def10;
   then reconsider a = t as Element of OU;
   reconsider p as Element of OU* by A3,A4,ZFMISC_1:106;
     [a,p] in REL(X) by A2,A4,LANG1:def 1;
   then a in [:the OperSymbols of S,{the carrier of S}:] by Def9;
   then consider o being OperSymbol of S,
                 x2 being Element of {the carrier of S} such that
A5:  a = [o,x2] by DOMAIN_1:9;
   take o;
   thus thesis by A5,TARSKI:def 1;
  end;
 uniqueness by ZFMISC_1:33;
end;

definition
 let S be non void non empty ManySortedSign,
    U0 be non-empty MSAlgebra over S,
    o be OperSymbol of S,
    p be FinSequence;
assume A1: p in Args(o,U0);
func pi(o,U0,p) -> Element of Union (the Sorts of U0) equals :Def23:
  Den(o,U0).p;
 coherence
  proof
   set F = Den(o,U0),
       S0 = the Sorts of U0,
       RS = the ResultSort of S,
       rs = the_result_sort_of o;
A2: dom F = Args(o,U0) & rng F c= Result(o,U0) by FUNCT_2:def 1,RELSET_1:12;
   then A3: F.p in rng F by A1,FUNCT_1:def 5;
      dom S0 = the carrier of S & rng RS c= the carrier of S
                        by PBOOLE:def 3,RELSET_1:12;
   then S0.rs in rng S0 by FUNCT_1:def 5;
   then F.p in union rng S0 by A2,A3,TARSKI:def 4;
   hence F.p is Element of Union S0 by PROB_1:def 3;
  end;
end;

theorem Th17:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S holds FreeGen(X) is free
proof
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
 set D = DTConMSA(X),
    FA = FreeMSA(X),
    FG = FreeGen(X);
 let U1 be non-empty MSAlgebra over S,
     F be ManySortedFunction of FG,the Sorts of U1;
 set SA =the Sorts of FA,
     AR = the Arity of S,
     S1 = the Sorts of U1,
     O = the OperSymbols of S,
     RS = the ResultSort of S,
     DU = Union (the Sorts of U1);
 A1: FA = MSAlgebra (# FreeSort(X), FreeOper(X) #) by Def16;
 deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1);

 deffunc NTermVal(Symbol of D, FinSequence,
 FinSequence) = pi(@(X,$1),U1,$3);

 consider G being Function of TS(D), DU such that
 A2: for t being Symbol of D st t in Terminals D
         holds G.(root-tree t) = TermVal(t) and
 A3: for nt be Symbol of D, ts be FinSequence of TS(D) st  nt ==> roots ts
          holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts)
          from DTConstrIndDef;
 deffunc F(set) = G | ((the Sorts of FA).$1);
 consider h be Function such that
 A4: dom h = the carrier of S &
 for s be set st s in the carrier of S holds h.s = F(s)
          from Lambda;
 reconsider h as ManySortedSet of the carrier of S by A4,PBOOLE:def 3;
   for s be set st s in dom h holds h.s is Function
  proof
   let s be set;
   assume s in dom h;
   then h.s = G | ((the Sorts of FA).s) by A4;
   hence thesis;
  end;
 then reconsider h as ManySortedFunction of the carrier of S by PRALG_1:def 15;
 defpred P[set] means
 for s be SortSymbol of S st $1 in (the Sorts of FA).s holds
  (h.s).$1 in (the Sorts of U1).s;
 A5: for t being Symbol of D st t in Terminals D holds P[root-tree t]
  proof
   let t be Symbol of D;
   assume A6: t in Terminals D;
   then consider s be SortSymbol of S, x be set such that
   A7: x in X.s & t = [x,s] by Th7;
   set E = {root-tree tt where tt is Symbol of D: tt in
 Terminals D & tt`2 = s},
       a = root-tree t;
   A8: t`2 = s by A7,MCART_1:7;
   then A9: a in E by A6;
   A10: E = FreeGen(s,X) & FreeGen(s,X) c= (FreeSort X).s by Th14;
   reconsider f = F.s as Function of FG.s,S1.s;
   A11: FG.s = E by A10,Def18;
   A12: dom f = FG.s & rng f c= S1.s by FUNCT_2:def 1,RELSET_1:12;
   then A13: f.a in rng f by A9,A11,FUNCT_1:def 5;
     h.s = G | (SA.s) by A4;
   then A14: (h.s).a = G.a by A1,A9,A10,FUNCT_1:72
    .= pi(F,S1,t) by A2,A6
    .= f.a by A6,A8,Def21;
   let s1 be SortSymbol of S;
   assume A15: a in SA.s1;
      now assume A16: s <> s1;
        a in (FreeSort X).s /\ (FreeSort X).s1 by A1,A9,A10,A15,XBOOLE_0:def 3;
      then (FreeSort X).s meets (FreeSort X).s1 by XBOOLE_0:4;
      hence contradiction by A16,Th13;
     end;
   hence thesis by A12,A13,A14;
  end;
 A17: for nt being Symbol of D,
       ts being FinSequence of TS(D) st nt ==> roots ts &
            for t being DecoratedTree of the carrier of D st t in rng ts
                      holds P[t]
    holds P[nt-tree ts]
   proof
    let nt be Symbol of D,
        ts be FinSequence of TS(D); assume
    A18: nt ==> roots ts &
       for t being DecoratedTree of the carrier of D st t in rng ts holds P[t];
    set p = G * ts,
        o = @(X,nt),
        ar = the_arity_of o,
        rs = the_result_sort_of o,
        OU = [:the OperSymbols of S,{the carrier of S}:] \/
             Union (coprod (X qua ManySortedSet of the carrier of S)),
        rt = roots ts;
    A19: o in O & ar = AR.o by MSUALG_1:def 6;
    A20: Args(o,U1) = (S1# * AR).o by MSUALG_1:def 9
                  .= product (S1 * ar) by A19,Th1;
    A21: dom p = dom ts & len p = len ts &
        for n be Nat st n in dom p holds p.n = G.(ts.n) by ALG_1:1;
    A22: dom rt = dom ts by DTCONSTR:def 1;
    A23: [o,the carrier of S] = nt by A18,Def22;
    A24: [o,the carrier of S] = Sym(o,X) by Def11;
    A25: rng ar c= the carrier of S & dom S1 = the carrier of S &
    dom SA = the carrier of S by FINSEQ_1:def 4,PBOOLE:def 3;
    then A26: dom(S1* ar) = dom ar & dom(SA* ar) = dom ar by RELAT_1:46;
    A27: [[o,the carrier of S],rt] in the Rules of D by A18,A23,LANG1:def 1;
    A28: D = DTConstrStr (# OU, REL(X) #) by Def10;
    then reconsider rt as Element of OU* by A27,ZFMISC_1:106;
    A29: len rt = len ar by A27,A28,Th5;
    A30: dom rt = Seg len rt & Seg len ar = dom ar by FINSEQ_1:def 3;
    then A31: dom p = dom (S1 * ar) by A21,A22,A26,A27,A28,Th5;
      for x st x in dom (S1 * ar) holds p.x in (S1 * ar).x
     proof
      let x;
      assume A32: x in dom (S1 * ar);
      then reconsider n = x as Nat by A26;
      A33: p.n = G.(ts.n) by A31,A32,ALG_1:1;
      A34: rng ts c= TS D by FINSEQ_1:def 4;
      A35: ts.n in rng ts by A22,A26,A29,A30,A32,FUNCT_1:def 5;
      then reconsider t = ts.n as Element of TS(D) by A34;
        ts in ((FreeSort X)# * AR).o by A18,A23,A24,Th10;
      then ts in product ((FreeSort X) * ar) by A19,Th1;
      then ts.x in ((FreeSort X) * ar).x by A1,A26,A32,CARD_3:18;
      then A36: ts.x in (FreeSort X).(ar.x) by A1,A26,A32,FUNCT_1:22;
        ar.x in rng ar by A26,A32,FUNCT_1:def 5;
      then reconsider s = ar.x as SortSymbol of S by A25;
      A37: (h.s).t in S1.s by A1,A18,A35,A36;
      A38: h.s = G | (SA.s) by A4;
      A39: dom G = TS D by FUNCT_2:def 1
               .= union rng SA by A1,Th12;
        dom SA = the carrier of S by PBOOLE:def 3;
      then SA.s in rng SA by FUNCT_1:def 5;
      then SA.s c= dom G by A39,ZFMISC_1:92;
      then dom (h.s) = SA.s by A38,RELAT_1:91;
      then G.t in S1.s by A1,A36,A37,A38,FUNCT_1:70;
      hence thesis by A32,A33,FUNCT_1:22;
     end;
    then A40: p in Args(o,U1) by A20,A21,A22,A26,A29,A30,CARD_3:18;
    then A41: pi(o,U1,p) = Den(o,U1).p by Def23;
    set ppi = pi(o,U1,p);
    A42: dom Den(o,U1) = Args(o,U1) & rng Den(o,U1) c= Result(o,U1)
      by FUNCT_2:def 1,RELSET_1:12;
    then ppi in rng Den(o,U1) by A40,A41,FUNCT_1:def 5;
    then A43: ppi in Result(o,U1) by A42;
      dom S1 = the carrier of S & rng RS c= the carrier of S &
    dom SA = the carrier of S by PBOOLE:def 3,RELSET_1:12;
    then A44: dom (S1 *RS) = dom RS & dom RS = O & dom (SA * RS) = dom RS
                                     by FUNCT_2:def 1,RELAT_1:46;
    A45: Result(o,U1) = (S1 *RS).o by MSUALG_1:def 10
        .= S1.(RS.o) by A44,FUNCT_1:22
        .= S1.rs by MSUALG_1:def 7;
    A46: G.(nt-tree ts) = ppi by A3,A18;
    A47: (DenOp(o,X)).ts = nt-tree ts by A18,A23,A24,Def14;
    A48: dom (DenOp (o,X)) = ((FreeSort X)# * AR).o &
    rng (DenOp (o,X)) c= ((FreeSort X) * RS).o by FUNCT_2:def 1,RELSET_1:12;
    then ts in dom (DenOp(o,X)) by A18,A23,A24,Th10;
    then nt-tree ts in rng (DenOp(o,X)) by A47,FUNCT_1:def 5;
    then nt-tree ts in (SA * RS).o by A1,A48;
    then nt-tree ts in SA.(RS.o) by A44,FUNCT_1:22;
    then A49: nt-tree ts in SA.rs by MSUALG_1:def 7;
    then A50: ppi = (G | (SA.rs)).(nt-tree ts) by A46,FUNCT_1:72;
    let s be SortSymbol of S;
    assume A51: nt-tree ts in SA.s;
       now
      assume A52: rs <> s;
        (FreeSort X).rs meets (FreeSort X).s by A1,A49,A51,XBOOLE_0:3;
      hence contradiction by A52,Th13;
     end;
    hence thesis by A4,A43,A45,A50;
   end;
 A53: for t being DecoratedTree of the carrier of D
       st t in TS(D) holds P[t] from DTConstrInd(A5,A17);

   for s be set st s in the carrier of S holds
         h.s is Function of (the Sorts of FA).s, (the Sorts of U1).s
  proof
   let x be set;
   assume x in the carrier of S;
   then reconsider s = x as SortSymbol of S;
   A54: h.s = G | (SA.s) by A4;
   A55: dom G = TS D by FUNCT_2:def 1
   .= union rng SA by A1,Th12;
     dom SA = the carrier of S by PBOOLE:def 3;
   then SA.s in rng SA by FUNCT_1:def 5;
   then A56: SA.s c= dom G by A55,ZFMISC_1:92;
   then A57: dom (h.s) = SA.s by A54,RELAT_1:91;
     rng (h.s) c= S1.s
    proof
     let a be set; assume
       a in rng (h.s);
     then consider T be set such that
     A58: T in dom (h.s) & (h.s).T = a by FUNCT_1:def 5;
     reconsider T as Element of TS(D) by A56,A57,A58,FUNCT_2:def 1;
       T in SA.s by A54,A56,A58,RELAT_1:91;
     hence thesis by A53,A58;
    end;
   hence thesis by A57,FUNCT_2:def 1,RELSET_1:11;
  end;
 then reconsider h as ManySortedFunction of FA,U1 by MSUALG_1:def 2;
 take h;
 thus h is_homomorphism FA,U1
  proof
   let o be OperSymbol of S such that Args(o,FA) <> {};
   let x be Element of Args(o,FA);
   set rs = the_result_sort_of o,
       DA = Den(o,FA),
       D1 = Den(o,U1),
       OU = [:the OperSymbols of S,{the carrier of S}:] \/
            Union (coprod (X qua ManySortedSet of the carrier of S)),
       ar = the_arity_of o;
   A59: DA = (FreeOper(X)).o by A1,MSUALG_1:def 11
         .= DenOp(o,X) by Def15;
   A60: Args(o,FA) = ((FreeSort X)# * AR).o by A1,MSUALG_1:def 9;
   then A61: x in ((FreeSort X)# * AR).o;
   reconsider p = x as FinSequence of TS(D) by A60,Th8;
   A62: Sym(o,X) ==> roots p by A60,Th10;
   then A63: DA.x = (Sym(o,X))-tree p by A59,Def14;
   A64: o in O & ar = AR.o & dom AR = O by FUNCT_2:def 1,MSUALG_1:def 6;
   A65: Sym(o,X) = [o,the carrier of S] &
      [@(X,Sym(o,X)),the carrier of S] = Sym(o,X) by A62,Def11,Def22;
then A66: @(X,Sym(o,X)) = o by ZFMISC_1:33;
     rng RS c= the carrier of S & dom SA = the carrier of S
             by PBOOLE:def 3,RELSET_1:12;
   then A67: dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:46;
   A68: (DenOp(o,X)).p = (Sym(o,X))-tree p by A62,Def14;
   A69: dom (DenOp (o,X)) = ((FreeSort X)# * AR).o &
   rng (DenOp (o,X)) c= ((FreeSort X) * RS).o by FUNCT_2:def 1,RELSET_1:12;
   then (Sym(o,X))-tree p in rng (DenOp(o,X)) by A60,A68,FUNCT_1:def 5;
   then (Sym(o,X))-tree p in (SA * RS).o by A1,A69;
   then (Sym(o,X))-tree p in SA.(RS.o) by A67,FUNCT_1:22;
   then A70: (Sym(o,X))-tree p in SA.rs by MSUALG_1:def 7;
   A71: h.rs = G | (SA.rs) by A4;
   A72: dom G = TS D by FUNCT_2:def 1
            .= union rng SA by A1,Th12;
   A73: dom (G *p) = dom p & len (G*p) = len p &
       for n be Nat st n in dom(G*p) holds (G*p).n = G.(p.n) by ALG_1:1;
   A74: dom (h#x) = dom ar & dom x = dom ar by MSUALG_3:6;
     for a be set st a in dom p holds (G*p).a = (h#x).a
    proof
     let a be set;
     assume A75: a in dom p;
     then reconsider n = a as Nat;
     A76: (G*p).n = G.(x.n) by A73,A75;
     A77: (h#x).n = (h.(ar/.n)).(x.n) by A75,MSUALG_3:def 8;
     A78: h.(ar/.n) = G | (SA.(ar/.n)) by A4;
     A79: p in product((FreeSort X) * ar) by A61,A64,Th1;
        rng ar c= the carrier of S & dom S1 = the carrier of S &
      dom SA = the carrier of S by FINSEQ_1:def 4,PBOOLE:def 3;
     then A80: dom(S1* ar) = dom ar & dom(SA* ar) = dom ar by RELAT_1:46;
     set rt = roots p;
     A81: dom rt = dom p by DTCONSTR:def 1;
     A82: [[o,the carrier of S],rt] in the Rules of D by A62,A65,LANG1:def 1;
     A83: D = DTConstrStr (# OU, REL(X) #) by Def10;
     then reconsider rt as Element of OU* by A82,ZFMISC_1:106;
     A84: len rt = len ar by A82,A83,Th5;
     A85: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3;
     then A86: p.n in ((FreeSort X) * ar).n by A1,A75,A79,A80,A81,A84,CARD_3:18
;
       ((FreeSort X) * ar).n = SA.(ar.n) by A1,A75,A80,A81,A84,A85,FUNCT_1:22
     .= SA.(ar/.n) by A75,A81,A84,A85,FINSEQ_4:def 4;
     hence thesis by A76,A77,A78,A86,FUNCT_1:72;
    end;
   then A87: G*p = h#x by A73,A74,FUNCT_1:9;
     dom SA = the carrier of S by PBOOLE:def 3;
   then SA.rs in rng SA by FUNCT_1:def 5;
   then SA.rs c= dom G by A72,ZFMISC_1:92;
   then dom (h.rs) = SA.rs by A71,RELAT_1:91;
   hence (h.rs).(DA.x) = G.((Sym(o,X))-tree p) by A63,A70,A71,FUNCT_1:70
   .= pi(@(X,Sym(o,X)),U1,G*p) by A3,A62
   .= D1.(h#x) by A66,A87,Def23;
  end;
   for x st x in the carrier of S holds (h || FG).x = F.x
  proof
   let x;
   assume x in the carrier of S;
   then reconsider s = x as SortSymbol of S;
   set hf = h || FG;
   A88: hf.s = (h.s) | (FG.s) by Def1;
   A89: dom (h.s) = SA.s by FUNCT_2:def 1;
   A90: FG.s = FreeGen(s,X) by Def18;
   A91: dom (hf.s) = FG.s by FUNCT_2:def 1;
   A92: dom (F.s) = FG.s by FUNCT_2:def 1;
     for a be set st a in FG.s holds (hf.s).a = (F.s).a
    proof
     let a be set;
     assume A93: a in FG.s;
     then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s
}
                                  by A90,Th14;
     then consider t be Symbol of D such that
     A94: a = root-tree t & t in Terminals D & t`2 = s;
     A95: h.s = G | (SA.s) by A4;
     thus (hf.s).a = (h.s).a by A88,A91,A93,FUNCT_1:70
     .= G.a by A1,A89,A90,A93,A95,FUNCT_1:70
     .= pi(F,S1,t) by A2,A94
     .= (F.s).a by A94,Def21;
    end;
   hence thesis by A91,A92,FUNCT_1:9;
  end;
 hence h || FG = F by PBOOLE:3;
end;

theorem Th18:
for S be non void non empty ManySortedSign,
    X be non-empty ManySortedSet of the carrier of S holds
FreeMSA(X) is free
proof
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
 take FreeGen(X);
 thus thesis by Th17;
end;

definition
 let S be non void non empty ManySortedSign;
cluster free strict (non-empty MSAlgebra over S);
 existence
  proof
   consider U1 be non-empty MSAlgebra over S;
   set X = the Sorts of U1;
   take FreeMSA(X);
   thus thesis by Th18;
  end;
end;

definition
 let S be non void non empty ManySortedSign,
    U0 be free MSAlgebra over S;
cluster free GeneratorSet of U0;
 existence by Def6;
end;

theorem Th19:
for S be non void non empty ManySortedSign,
    U1 be non-empty MSAlgebra over S
 ex U0 be strict free (non-empty MSAlgebra over S),
    F be ManySortedFunction of U0,U1
       st F is_epimorphism U0,U1
 proof
  let S be non void non empty ManySortedSign,
     U1 be non-empty MSAlgebra over S;
  set S1 = the Sorts of U1,
      FA = FreeMSA(S1),
      FG = FreeGen(S1);
  A1: FG is free by Th17;
  set f = Reverse(S1);
  consider F be ManySortedFunction of FA,U1 such that
  A2: F is_homomorphism FA,U1 & F || FG = f
           by A1,Def5;
  reconsider fa = FA as strict free (non-empty MSAlgebra over S) by Th18;
  reconsider a = F as ManySortedFunction of fa,U1;
  take fa;
  take a;
  thus a is_homomorphism fa,U1 by A2;
  thus a is "onto"
   proof
    let s be set;
    assume s in the carrier of S;
    then reconsider s0 = s as SortSymbol of S;
    reconsider g = a.s as Function of (the Sorts of fa).s0, S1.s0
       by MSUALG_1:def 2;
    A3: f.s0 = g | (FG.s0) by A2,Def1;
    then A4: rng (f.s0) c= rng g by FUNCT_1:76;
    thus rng (a.s) c= S1.s by A3,RELSET_1:12;
    let x be set;
    assume A5: x in S1.s;
    set D = DTConMSA(S1),
        t = [x,s0];
    A6: t in Terminals D by A5,Th7;
    then reconsider t as Symbol of D;
    A7: f.s0 = Reverse(s0,S1) by Def20;
    then A8: dom (f.s0) = FreeGen(s0,S1) by FUNCT_2:def 1;
      t`2 = s0 by MCART_1:7;
    then root-tree t in {root-tree tt where tt is Symbol of D :
                                  tt in Terminals D & tt`2 = s0} by A6;
    then A9: root-tree t in FreeGen(s0,S1) by Th14;
    then A10: (f.s0).(root-tree t) in rng (f.s0) by A8,FUNCT_1:def 5;
      (f.s0).(root-tree t) = t`1 by A7,A9,Def19
    .= x by MCART_1:7;
    hence thesis by A4,A10;
   end;
 end;

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

Back to top