:: Free Universal Algebra Construction
::  by Beata Perkowska
::
:: Received October 20, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XBOOLE_0, ARYTM_1, CARD_1, RELAT_1, FINSEQ_1,
      QUANTAL1, UNIALG_1, UNIALG_2, FUNCT_1, MSAFREE, TARSKI, STRUCT_0,
      FINSEQ_2, PRELAMB, CQC_SIM1, MSUALG_3, FUNCOP_1, PARTFUN1, FUNCT_2,
      NAT_1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, CARD_3, TREES_2,
      QC_LANG1, FREEALG;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, ORDINAL1, RELAT_1,
      RELSET_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, FUNCOP_1, FINSEQ_2,
      TREES_2, TREES_3, TREES_4, MARGREL1, STRUCT_0, UNIALG_1, UNIALG_2, LANG1,
      DTCONSTR, PRE_POLY, ALG_1;
 constructors DOMAIN_1, FINSEQOP, DTCONSTR, ALG_1, RELSET_1, PRE_POLY;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, XREAL_0,
      FINSEQ_1, FINSEQ_2, TREES_3, STRUCT_0, UNIALG_2, DTCONSTR, CARD_1,
      RELSET_1, MARGREL1, FUNCT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, UNIALG_2, DTCONSTR, XBOOLE_0, FINSEQ_2, FUNCOP_1,
      MARGREL1;
 theorems FINSEQ_1, FINSEQ_2, PARTFUN1, FUNCT_1, FUNCT_2, NAT_1, ZFMISC_1,
      UNIALG_1, ALG_1, TARSKI, FUNCOP_1, UNIALG_2, LANG1, DTCONSTR, RELAT_1,
      XBOOLE_0, XBOOLE_1, TREES_3, MARGREL1, FINSEQ_3, CARD_1;
 schemes PARTFUN1, FINSEQ_1, RELSET_1, DTCONSTR;

begin

::
:: Preliminaries
::

reserve x,y for set,
  n for Element of NAT;

definition
  let IT be set;
  attr IT is disjoint_with_NAT means
  :Def1:
  IT misses NAT;
end;

registration
  cluster non empty disjoint_with_NAT for set;
  existence
  proof
    take X = {-1};
    thus X is non empty;
    now
      assume X meets NAT;
      then consider x such that
A1:   x in X and
A2:   x in NAT by XBOOLE_0:3;
      reconsider x as Element of NAT by A2;
      x = -1 by A1,TARSKI:def 1;
      hence contradiction by NAT_1:2;
    end;
    hence thesis by Def1;
  end;
end;

Lm1: not 0 in rng <*1*> & 0 in rng <*0*>
proof
  rng <*0*> = {0} & rng <*1*> = {1} by FINSEQ_1:38;
  hence thesis by TARSKI:def 1;
end;

notation
  let IT be Relation;
  antonym IT is with_zero for IT is non-empty;
  synonym IT is without_zero for IT is non-empty;
end;

definition
  let IT be Relation;
  redefine attr IT is with_zero means
  :Def2:
  0 in rng IT;
  compatibility by RELAT_1:def 9;
end;

registration
  cluster non empty with_zero for FinSequence of NAT;
  existence
  proof
    reconsider f = <*0*> as FinSequence of NAT;
    take f;
    thus f is non empty;
    thus 0 in rng f by Lm1;
  end;
  cluster non empty without_zero for FinSequence of NAT;
  existence
  proof
    reconsider f = <*1*> as FinSequence of NAT;
    take f;
    thus f is non empty;
    thus not 0 in rng f by Lm1;
  end;
end;

begin

::
:: Free Universal Algebra - General Notions
::

definition
  let U1 be Universal_Algebra, n be Element of NAT;
  assume
A1: n in dom (the charact of U1);

  func oper(n,U1) -> operation of U1 equals
  :Def3:
  (the charact of U1).n;
  coherence by A1,FUNCT_1:def 3;
end;

definition
  let U0 be Universal_Algebra;
  mode GeneratorSet of U0 -> Subset of U0 means
    for A being Subset of U0 st A
    is opers_closed & it c= A holds A = the carrier of U0;
  existence
  proof
    the carrier of U0 c= the carrier of U0;
    then reconsider GG = the carrier of U0 as non empty Subset of U0;
    take GG;
    thus thesis by XBOOLE_0:def 10;
  end;
end;

Lm2: for A being Universal_Algebra for B being Subset of A st B is
opers_closed holds Constants A c= B
proof
  let A be Universal_Algebra;
  let B be Subset of A such that
A1: B is opers_closed;
  let x be set;
  assume x in Constants A;
  then consider a being Element of A such that
A2: x = a and
A3: ex o being Element of Operations A st arity o = 0 & a in rng o;
  consider o being Element of Operations A such that
A4: arity o = 0 and
A5: a in rng o by A3;
A6: B is_closed_on o by A1,UNIALG_2:def 4;
  consider s being set such that
A7: s in dom o and
A8: a = o.s by A5,FUNCT_1:def 3;
  reconsider s as Element of (the carrier of A)* by A7;
A9: dom o = 0-tuples_on the carrier of A by A4,MARGREL1:22;
  then s = {} by A7;
  then rng s c= B by RELAT_1:38,XBOOLE_1:2;
  then
A10: s is FinSequence of B by FINSEQ_1:def 4;
  len s = 0 by A7,A9;
  hence thesis by A2,A4,A8,A10,A6,UNIALG_2:def 3;
end;

Lm3: for A being Universal_Algebra for B being Subset of A st B <> {} or
Constants A <> {} holds B is GeneratorSet of A iff the carrier of GenUnivAlg B
= the carrier of A
proof
  let A be Universal_Algebra;
  let G be Subset of A;
  assume
A1: G <> {} or Constants A <> {};
  thus G is GeneratorSet of A implies the carrier of GenUnivAlg G = the
  carrier of A
  proof
    reconsider C = the carrier of GenUnivAlg G as non empty Subset of A by
UNIALG_2:def 7;
    assume
A2: for B being Subset of A st B is opers_closed & G c= B holds B =
    the carrier of A;
    G c= C & C is opers_closed by A1,UNIALG_2:def 7,def 12;
    hence thesis by A2;
  end;
  assume
A3: the carrier of GenUnivAlg G = the carrier of A;
  let B be Subset of A such that
A4: B is opers_closed and
A5: G c= B;
  reconsider C = B as non empty Subset of A by A1,A4,A5,Lm2,XBOOLE_1:3;
  thus B c= the carrier of A;
A6: UniAlgSetClosed C = UAStr(#C,Opers(A,C)#) by A4,UNIALG_2:def 8;
  then GenUnivAlg G is SubAlgebra of UniAlgSetClosed C by A1,A5,UNIALG_2:def 12
;
  then the carrier of A is Subset of C by A3,A6,UNIALG_2:def 7;
  hence thesis;
end;

definition
  let U0 be Universal_Algebra;
  let IT be GeneratorSet of U0;
  attr IT is free means
  :Def5:
  for U1 be Universal_Algebra st U0,U1
are_similar holds for f be Function of IT,the carrier of U1 ex h be Function of
  U0,U1 st h is_homomorphism U0,U1 & h|IT = f;
end;

definition
  let IT be Universal_Algebra;
  attr IT is free means
  :Def6:
  ex G being GeneratorSet of IT st G is free;
end;

registration
  cluster free strict for Universal_Algebra;
  existence
  proof
    set x = the set;
    reconsider A = {x} as non empty set;
    set a = the Element of A;
    reconsider w = <*>A .--> a as Element of PFuncs(A*,A) by MARGREL1:19;
    reconsider ww = <*w*> as PFuncFinSequence of A;
    set U0 = UAStr (# A, ww#);
A1: the charact of(U0) is quasi_total & the charact of(U0) is homogeneous
    by MARGREL1:20;
A2: the charact of(U0) is non-empty by MARGREL1:20;
A3: len the charact of(U0) = 1 by FINSEQ_1:39;
    reconsider U0 as Universal_Algebra by A1,A2,UNIALG_1:def 1,def 2,def 3;
A4: dom the charact of(U0) = {1} by A3,FINSEQ_1:2,def 3;
    1 in {1} by TARSKI:def 1;
    then reconsider o0 = (the charact of U0).1 as operation of U0 by A4,
FUNCT_1:def 3;
    take U0;
A5: GenUnivAlg( {}(the carrier of U0) ) = U0
    proof
      set P = {}(the carrier of U0);
      reconsider B = the carrier of GenUnivAlg(P) as non empty Subset of U0 by
UNIALG_2:def 7;
A6:   dom the charact of(U0) = dom Opers(U0,B) by UNIALG_2:def 6;
A7:   B = the carrier of U0 by ZFMISC_1:33;
      for n be Nat st n in dom the charact of(U0) holds (the charact of(
      U0)).n =(Opers(U0,B)).n
      proof
        let n be Nat;
        assume
A8:     n in dom the charact of(U0);
        then reconsider o =(the charact of(U0)).n as operation of U0 by
FUNCT_1:def 3;
        (Opers(U0,B)).n = o/.B by A6,A8,UNIALG_2:def 6;
        hence thesis by A7,UNIALG_2:4;
      end;
      then the charact of(U0) = Opers(U0,B) by A6,FINSEQ_1:13
        .= the charact of GenUnivAlg(P) by UNIALG_2:def 7;
      hence thesis by A7;
    end;
A9: o0 = w by FINSEQ_1:40;
    then
A10: dom o0 = {<*>A} by FUNCOP_1:13;
    now
      <*>A in dom o0 by A10,TARSKI:def 1;
      hence ex x being FinSequence st x in dom o0;
      let x be FinSequence;
      assume x in dom o0;
      then x = <*>A by A10,TARSKI:def 1;
      hence len x = 0;
    end;
    then
A11: arity o0 = 0 by MARGREL1:def 25;
A12: {} in {<*>A} by TARSKI:def 1;
    then o0.<*>A = a by A9,FUNCOP_1:7;
    then a in rng o0 by A10,A12,FUNCT_1:def 3;
    then a in Constants U0 by A11;
    then reconsider G = {}(the carrier of U0) as GeneratorSet of U0 by A5,Lm3;
    now
      take G;
      now
        let U1 be Universal_Algebra;
A13:    1 in {1} by TARSKI:def 1;
        assume
A14:    U0,U1 are_similar;
        then
A15:    signature U0 = signature U1 by UNIALG_2:def 1;
        len the charact of(U1) = 1 by A3,A14,UNIALG_2:1;
        then dom the charact of(U1) = {1} by FINSEQ_1:2,def 3;
        then reconsider o1 = (the charact of U1).1 as operation of U1 by A13,
FUNCT_1:def 3;
A16:    rng o1 c= the carrier of U1 by RELAT_1:def 19;
        let f be Function of G,the carrier of U1;
        consider aa be set such that
A17:    aa in dom o1 by XBOOLE_0:def 1;
        o1.aa in rng o1 by A17,FUNCT_1:def 3;
        then reconsider u1 = o1.aa as Element of U1 by A16;
        reconsider h = (the carrier of U0) --> u1 as Function of U0,U1;
        take h;
A18:    len (signature U0) = len the charact of(U0) & dom (signature U0)
        = Seg len ( signature U0) by FINSEQ_1:def 3,UNIALG_1:def 4;
        then (signature U0).1 = arity o0 by A3,A13,FINSEQ_1:2,UNIALG_1:def 4;
        then
A19:    arity o0 = arity o1 by A3,A13,A15,A18,FINSEQ_1:2,UNIALG_1:def 4;
        now
          let n be Element of NAT;
          assume n in dom the charact of(U0);
          then
A20:      n = 1 by A4,TARSKI:def 1;
          let 0o be operation of U0,1o be operation of U1;
          assume that
A21:      0o=(the charact of U0).n and
A22:      1o=(the charact of U1).n;
          let y be FinSequence of U0;
          assume
A23:      y in dom 0o;
          then y = <*>the carrier of U0 by A10,A20,A21,TARSKI:def 1;
          then
A24:      h*y = <*>the carrier of U1;
          dom 1o = 0-tuples_on the carrier of U1 by A11,A19,A20,A22,MARGREL1:22
            .= {<*>the carrier of U1} by FINSEQ_2:94;
          then
A25:      1o.(h*y) = u1 by A17,A20,A22,A24,TARSKI:def 1;
A26:      rng 0o c= the carrier of U0 by RELAT_1:def 19;
          0o.y in rng 0o by A23,FUNCT_1:def 3;
          hence h.(0o.y) = 1o.(h*y) by A25,A26,FUNCOP_1:7;
        end;
        hence h is_homomorphism U0,U1 by A14,ALG_1:def 1;
        f = {};
        hence h|G = f;
      end;
      hence G is free by Def5;
    end;
    hence thesis by Def6;
  end;
end;

registration
  let U0 be free Universal_Algebra;
  cluster free for GeneratorSet of U0;
  existence by Def6;
end;

theorem
  for U0 be strict Universal_Algebra,A be Subset of U0 st Constants U0
  <> {} or A <> {} holds A is GeneratorSet of U0 iff GenUnivAlg(A) = U0
proof
  let U0 be strict Universal_Algebra,A be Subset of U0 such that
A1: Constants U0 <> {} or A <> {};
  thus A is GeneratorSet of U0 implies GenUnivAlg(A) = U0
  proof
    assume A is GeneratorSet of U0;
    then
A2: the carrier of GenUnivAlg(A) = the carrier of U0 by A1,Lm3;
    U0 is strict SubAlgebra of U0 by UNIALG_2:8;
    hence thesis by A2,UNIALG_2:12;
  end;
  assume GenUnivAlg(A) = U0;
  hence thesis by A1,Lm3;
end;

begin

::
:: Construction of a Decorated Tree Structure for Free Universal Algebra
::

definition
  let f be non empty FinSequence of NAT, X be set;
  func REL(f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X)*) means
  :Def7:
  for a be Element of (dom f) \/ X, b be Element of ((dom f) \/ X)* holds [a,b]
  in it iff a in dom f & f.a = len b;
  existence
  proof
    set A = (dom f) \/ X;
    defpred P[Element of A, Element of A*] means $1 in dom f & f.$1 = len $2;
    consider R being Relation of A,A* such that
A1: for x being (Element of A), y being Element of A* holds [x,y] in R
    iff P[x,y] from RELSET_1:sch 2;
    take R;
    let a be Element of A, b be Element of A*;
    thus thesis by A1;
  end;
  uniqueness
  proof
    set A = (dom f) \/ X;
    let R,T be Relation of A,A*;
    assume that
A2: for a be Element of A, b be Element of A* holds [a,b] in R iff a
    in dom f & f.a = len b and
A3: for a be Element of A, b be Element of A* holds [a,b] in T iff a
    in dom f & f.a = len b;
    for x,y holds [x,y] in R iff [x,y] in T
    proof
      let x,y;
      thus [x,y] in R implies [x,y] in T
      proof
        assume
A4:     [x,y] in R;
        then reconsider x1=x as Element of A by ZFMISC_1:87;
        reconsider y1=y as Element of A* by A4,ZFMISC_1:87;
        [x1,y1] in R by A4;
        then
A5:     x1 in dom f by A2;
        f.x1 = len y1 by A2,A4;
        hence thesis by A3,A5;
      end;
      assume
A6:   [x,y] in T;
      then reconsider x1=x as Element of A by ZFMISC_1:87;
      reconsider y1=y as Element of A* by A6,ZFMISC_1:87;
      [x1,y1] in T by A6;
      then
A7:   x1 in dom f by A3;
      f.x1 = len y1 by A3,A6;
      hence thesis by A2,A7;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

definition
  let f be non empty FinSequence of NAT, X be set;
  func DTConUA(f,X) -> strict DTConstrStr equals
  DTConstrStr (# (dom f) \/ X,
    REL(f,X) #);
  correctness;
end;

registration
  let f be non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> non empty;
  coherence;
end;

theorem Th2:
  for f be non empty FinSequence of NAT, X be set holds (Terminals
  (DTConUA(f,X))) c= X & NonTerminals(DTConUA(f,X)) = dom f
proof
  let f be non empty FinSequence of NAT, X be set;
  set A = DTConUA(f,X), D = (dom f) \/ X;
A1: the carrier of A = (Terminals A) \/ (NonTerminals A) by LANG1:1;
  (Terminals A) misses (NonTerminals A) by DTCONSTR:8;
  then
A2: (Terminals A) /\ (NonTerminals A) = {} by XBOOLE_0:def 7;
  thus Terminals A c= X
  proof
    let x;
    assume
A3: x in Terminals A;
    then reconsider xd = x as Element of D by A1,XBOOLE_0:def 3;
    reconsider xa = x as Element of (the carrier of A) by A1,A3,XBOOLE_0:def 3;
A4: now
A5:   rng f c= NAT by FINSEQ_1:def 4;
      assume
A6:   x in dom f;
      then f.x in rng f by FUNCT_1:def 3;
      then reconsider fx = f.x as Element of NAT by A5;
      reconsider a = fx |-> xd as FinSequence of D;
      reconsider a as Element of D* by FINSEQ_1:def 11;
      len a = f.xd by CARD_1:def 7;
      then [xd,a] in REL(f,X) by A6,Def7;
      then xa ==> a by LANG1:def 1;
      then xa in { t where t is Symbol of A: ex n be FinSequence st t ==> n};
      then x in NonTerminals A by LANG1:def 3;
      hence contradiction by A2,A3,XBOOLE_0:def 4;
    end;
    x in (dom f) \/ X by A1,A3,XBOOLE_0:def 3;
    hence thesis by A4,XBOOLE_0:def 3;
  end;
  thus NonTerminals A c= dom f
  proof
    let x;
    assume x in NonTerminals A;
    then x in {t where t is Symbol of A: ex n be FinSequence st t ==> n} by
LANG1:def 3;
    then consider t be Symbol of A such that
A7: x = t and
A8: ex n be FinSequence st t ==> n;
    consider n be FinSequence such that
A9: t ==>n by A8;
    [t,n] in the Rules of A by A9,LANG1:def 1;
    then reconsider n as Element of D* by ZFMISC_1:87;
    reconsider t as Element of D;
    [t,n] in REL(f,X) by A9,LANG1:def 1;
    hence thesis by A7,Def7;
  end;
  let x;
A10: rng f c= NAT by FINSEQ_1:def 4;
  assume
A11: x in dom f;
  then reconsider xa = x as Symbol of A by XBOOLE_0:def 3;
  f.x in rng f by A11,FUNCT_1:def 3;
  then reconsider fx = f.x as Element of NAT by A10;
  reconsider xd = x as Element of D by A11,XBOOLE_0:def 3;
  reconsider a = fx |-> xd as FinSequence of D;
  reconsider a as Element of D* by FINSEQ_1:def 11;
  len a = f.xd by CARD_1:def 7;
  then [xd,a] in REL(f,X) by A11,Def7;
  then xa ==> a by LANG1:def 1;
  then xa in { t where t is Symbol of A: ex n be FinSequence st t ==> n};
  hence thesis by LANG1:def 3;
end;

theorem Th3:
  for f be non empty FinSequence of NAT, X be disjoint_with_NAT set
  holds (Terminals (DTConUA(f,X))) = X
proof
  let f be non empty FinSequence of NAT, X be disjoint_with_NAT set;
  set A = DTConUA(f,X);
  thus Terminals A c= X by Th2;
  let x;
  assume
A1: x in X;
A2: NonTerminals A = dom f by Th2;
A3: now
    assume x in NonTerminals A;
    then X meets NAT by A2,A1,XBOOLE_0:3;
    hence contradiction by Def1;
  end;
  the carrier of A = (Terminals A) \/ (NonTerminals A) & x in (dom f) \/ X
  by A1,LANG1:1,XBOOLE_0:def 3;
  hence thesis by A3,XBOOLE_0:def 3;
end;

registration
  let f be non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> with_nonterminals;
  coherence
  proof
    NonTerminals DTConUA(f,X) = dom f by Th2;
    hence thesis by DTCONSTR:def 4;
  end;
end;

registration
  let f be with_zero non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> with_nonterminals with_useful_nonterminals;
  coherence
  proof
    set A = DTConUA(f,X), D = (dom f) \/ X;
    A is with_useful_nonterminals
    proof
      set e = <*>(TS A);
      let s be Symbol of A;
      assume
A1:   s in NonTerminals A;
A2:   rng f c= NAT by FINSEQ_1:def 4;
      NonTerminals A = dom f by Th2;
      then f.s in rng f by A1,FUNCT_1:def 3;
      then reconsider fs = f.s as Element of NAT by A2;
      reconsider sd = s as Element of D;
      roots e = <*> D by DTCONSTR:3;
      then reconsider re = (roots e) as Element of D*;
      0 in rng f by Def2;
      then consider x such that
A3:   x in dom f and
A4:   f.x = 0 by FUNCT_1:def 3;
A5:   NonTerminals A = dom f by Th2;
      then reconsider s0 = x as Symbol of A by A3;
      set p = fs |-> (s0-tree e);
A6:   len p = fs by CARD_1:def 7;
      len re = 0 by DTCONSTR:3;
      then [s0,roots e] in the Rules of A by A3,A4,Def7;
      then s0 ==> roots e by LANG1:def 1;
      then
A7:   s0-tree(e) in (TS A) by DTCONSTR:def 1;
A8:   rng p c= TS A
      proof
        let y;
        assume y in rng p;
        then
A9:     ex n being Nat st n in dom p & p.n = y by FINSEQ_2:10;
        dom p = Seg len p by FINSEQ_1:def 3;
        hence thesis by A7,A6,A9,FUNCOP_1:7;
      end;
      dom(roots p) = dom p by TREES_3:def 18
        .= Seg len p by FINSEQ_1:def 3;
      then
A10:  len(roots p) = fs by A6,FINSEQ_1:def 3;
      reconsider p as FinSequence of TS A by A8,FINSEQ_1:def 4;
      take p;
      reconsider p as FinSequence of FinTrees the carrier of A;
      reconsider rp =roots p as Element of D* by FINSEQ_1:def 11;
      [sd,rp] in REL(f,X) by A1,A5,A10,Def7;
      hence thesis by LANG1:def 1;
    end;
    hence thesis;
  end;
end;

registration
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  cluster DTConUA(f,D) -> with_terminals with_nonterminals
    with_useful_nonterminals;
  coherence
  proof
    set A = DTConUA(f,D);
A1: NonTerminals A = dom f by Th2;
A2: Terminals A = D by Th3;
    A is with_useful_nonterminals
    proof
      set d = the Element of D;
      let s be Symbol of A;
      reconsider sd = d as Symbol of A by XBOOLE_0:def 3;
A3:   rng f c= NAT by FINSEQ_1:def 4;
      assume
A4:   s in NonTerminals A;
      then f.s in rng f by A1,FUNCT_1:def 3;
      then reconsider fs = f.s as Element of NAT by A3;
      reconsider sdd = s as Element of ((dom f) \/ D);
      set p = fs |-> (root-tree sd);
A5:   len p = fs by CARD_1:def 7;
A6:   root-tree sd in TS(A) by A2,DTCONSTR:def 1;
A7:   rng p c= TS A
      proof
        let y;
        assume y in rng p;
        then consider n being Nat such that
A8:     n in dom p and
A9:     p.n = y by FINSEQ_2:10;
        n in Seg len p by A8,FINSEQ_1:def 3;
        hence thesis by A6,A5,A9,FUNCOP_1:7;
      end;
      dom(roots p) = dom p by TREES_3:def 18
        .= Seg len p by FINSEQ_1:def 3;
      then
A10:  len(roots p) = fs by A5,FINSEQ_1:def 3;
      reconsider p as FinSequence of (TS A) by A7,FINSEQ_1:def 4;
      take p;
      reconsider p as FinSequence of FinTrees the carrier of A;
      reconsider rp =(roots p) as Element of ((dom f) \/ D)* by FINSEQ_1:def 11
;
      [sdd,rp] in REL(f,D) by A1,A4,A10,Def7;
      hence thesis by LANG1:def 1;
    end;
    hence thesis by A2,DTCONSTR:def 3;
  end;
end;

definition
  let f be non empty FinSequence of NAT, X be set, n be Nat;
  assume
A1: n in dom f;
  func Sym(n,f,X) -> Symbol of DTConUA(f,X) equals
  :Def9:
  n;
  coherence by A1,XBOOLE_0:def 3;
end;

begin

::
:: Construction of Free Universal Algebra for Non Empty Set of Generators and
::                           Given Signature

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set,
  n be Nat;
  assume
A1: n in dom f;
  func FreeOpNSG(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
  DTConUA(f,D))*, TS(DTConUA(f,D)) means
  :Def10:
  dom it = (f/.n)-tuples_on TS(
  DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
  it.p = Sym(n,f,D)-tree(p);
  existence
  proof
    set A = DTConUA(f,D), i = f/.n, Y = (dom f) \/ D, smm = Sym(n,f,D);
    defpred P[set,set] means $1 in i-tuples_on (TS A) & for p be FinSequence
    of (TS A) st p = $1 holds $2 = smm-tree(p);
    set tu = {s where s is Element of (TS A)*: len s = f/.n};
A2: i = f.n by A1,PARTFUN1:def 6;
A3: for x,y st x in (TS A)* & P[x,y] holds y in (TS A)
    proof
      reconsider sm = Sym(n,f,D) as Element of Y;
      let x,y;
      assume that
      x in (TS A)* and
A4:   P[x,y];
      consider s be Element of (TS A)* such that
A5:   s = x and
A6:   len s = i by A4;
A7:   y = Sym(n,f,D)-tree(s) by A4,A5;
      reconsider s as FinSequence of (TS A);
      dom (roots s) = dom s & Seg len (roots s) = dom(roots s) by
FINSEQ_1:def 3,TREES_3:def 18;
      then
A8:   len (roots s) = i by A6,FINSEQ_1:def 3;
      reconsider s as FinSequence of FinTrees the carrier of A;
      reconsider rs = roots s as Element of Y* by FINSEQ_1:def 11;
      sm = n by A1,Def9;
      then [sm,rs] in REL(f,D) by A1,A2,A8,Def7;
      then Sym(n,f,D) ==> roots s by LANG1:def 1;
      hence thesis by A7,DTCONSTR:def 1;
    end;
A9: for x,y1,y2 be set st x in (TS A)* & P[x,y1] & P[x,y2] holds y1 = y2
    proof
      let x,y1,y2 be set;
      assume that
      x in (TS A)* and
A10:  P[x,y1] and
A11:  P[x,y2];
      consider s be Element of (TS A)* such that
A12:  s = x and
      len s = i by A10;
      y1 = Sym(n,f,D)-tree(s) by A10,A12;
      hence thesis by A11,A12;
    end;
    consider F being PartFunc of (TS A)*,(TS A) such that
A13: for x be set holds x in dom F iff x in (TS A)* & ex y st P[x,y] and
A14: for x be set st x in dom F holds P[x,F.x] from PARTFUN1:sch 2(A3,
    A9);
A15: dom F = i-tuples_on (TS A)
    proof
      thus dom F c= i-tuples_on(TS A)
      proof
        let x;
        assume x in dom F;
        then ex y st P[x,y] by A13;
        hence thesis;
      end;
      reconsider sm = smm as Symbol of A;
      let x;
      assume x in i-tuples_on(TS A);
      then consider s be Element of (TS A)* such that
A16:  s = x and
A17:  len s = i;
      P[s,sm-tree(s)] by A17;
      hence thesis by A13,A16;
    end;
A18: for x,y be FinSequence of TS(A) st len x=len y & x in dom F holds y
    in dom F
    proof
      let x,y be FinSequence of TS(A);
      assume that
A19:  len x = len y and
A20:  x in dom F;
      reconsider sy = y as Element of (TS A)* by FINSEQ_1:def 11;
      ex sx be Element of (TS A)* st sx = x & len sx = f/.n by A15,A20;
      then sy in tu by A19;
      hence thesis by A15;
    end;
A21:   ex x being FinSequence st x in dom F
     proof
      set a = the Element of i-tuples_on(TS A);
      a in dom F by A15;
      hence ex x being FinSequence st x in dom F;
     end;
    dom F is with_common_domain
     proof
      let x,y be FinSequence;
      assume x in dom F & y in dom F;
      then (ex sx be Element of (TS A)* st sx = x & len sx = f/.n )& ex sy be
      Element of (TS A)* st sy = y & len sy = f/.n by A15;
      hence thesis;
    end;
    then reconsider
    F as homogeneous quasi_total non empty PartFunc of (TS A)*, TS(
    A) by A18,A21,MARGREL1:def 21,def 22;
    take F;
    thus dom F = i-tuples_on (TS A) by A15;
    let p be FinSequence of (TS A);
    assume p in dom F;
    hence thesis by A14;
  end;
  uniqueness
  proof
    set A = TS DTConUA(f,D);
    let f1,f2 be homogeneous quasi_total non empty PartFunc of A*,A;
    assume that
A22: dom f1 = (f/.n)-tuples_on A and
A23: for p be FinSequence of A st p in dom f1 holds f1.p = Sym(n,f,D)
    -tree(p) and
A24: dom f2 = (f/.n)-tuples_on A and
A25: for p be FinSequence of A st p in dom f2 holds f2.p = Sym(n,f,D) -tree(p);
    now
      let x;
      assume
A26:  x in (f/.n)-tuples_on A;
      then consider s be Element of A* such that
A27:  s = x and
      len s = f/.n;
      f1.s = Sym(n,f,D)-tree(s) by A22,A23,A26,A27;
      hence f1.x = f2.x by A24,A25,A26,A27;
    end;
    hence thesis by A22,A24,FUNCT_1:2;
  end;
end;

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  func FreeOpSeqNSG(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
  :Def11:
  len it = len f & for n st n in dom it holds it.n = FreeOpNSG(n,f,D);
  existence
  proof
    defpred P[Nat,set] means $2 = FreeOpNSG($1,f,D);
    set A = TS(DTConUA(f,D));
A1: for n be Nat st n in Seg len f ex x be Element of PFuncs(A*,A) st P[n, x]
    proof
      let n be Nat;
      assume n in Seg len f;
      reconsider O=FreeOpNSG(n,f,D) as Element of PFuncs(A*,A) by PARTFUN1:45;
      take O;
      thus thesis;
    end;
    consider p be FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len f & for n be Nat st n in Seg len f holds P[n,p.n]
    from FINSEQ_1:sch 5(A1);
    reconsider p as PFuncFinSequence of A;
    take p;
    thus len p = len f by A2,FINSEQ_1:def 3;
    let n;
    assume n in dom p;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f1,f2 be PFuncFinSequence of TS DTConUA(f,D);
    assume that
A3: len f1 = len f and
A4: for n st n in dom f1 holds f1.n = FreeOpNSG(n,f,D) and
A5: len f2 = len f and
A6: for n st n in dom f2 holds f2.n = FreeOpNSG(n,f,D);
    for n being Nat st n in dom f1 holds f1.n = f2.n
    proof
      let n be Nat;
A7:   dom f1 = Seg len f1 & dom f2 = Seg len f2 by FINSEQ_1:def 3;
      assume
A8:   n in dom f1;
      then f1.n = FreeOpNSG(n,f,D) by A4;
      hence thesis by A3,A5,A6,A7,A8;
    end;
    hence thesis by A3,A5,FINSEQ_2:9;
  end;
end;

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  func FreeUnivAlgNSG(f,D) -> strict Universal_Algebra equals
  UAStr (# TS(
    DTConUA(f,D)), FreeOpSeqNSG(f,D)#);
  coherence
  proof
    set A = TS DTConUA(f,D), AA = UAStr (# A, FreeOpSeqNSG(f,D) #);
    for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
    = (the charact of AA).n holds h is quasi_total
    proof
      let n be Nat,h be PartFunc of A*,A;
      assume n in dom the charact of(AA) & h = (the charact of AA).n;
      then h = FreeOpNSG(n,f,D) by Def11;
      hence thesis;
    end;
    then
A1: the charact of(AA) is quasi_total by MARGREL1:def 24;
    for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
    = (the charact of AA).n holds h is homogeneous
    proof
      let n be Nat,h be PartFunc of A*,A;
      assume n in dom the charact of(AA) & h = (the charact of AA).n;
      then h = FreeOpNSG(n,f,D) by Def11;
      hence thesis;
    end;
    then
A2: the charact of(AA) is homogeneous by MARGREL1:def 23;
    for n be set st n in dom the charact of(AA) holds (the charact of AA)
    .n is non empty
    proof
      let n be set;
      assume
A3:   n in dom the charact of(AA);
      then reconsider n as Element of NAT;
      (the charact of AA).n = FreeOpNSG(n,f,D) by A3,Def11;
      hence thesis;
    end;
    then
A4: the charact of(AA) is non-empty by FUNCT_1:def 9;
    len FreeOpSeqNSG(f,D) = len f by Def11;
    then the charact of(AA) <> {};
    hence thesis by A1,A2,A4,UNIALG_1:def 1,def 2,def 3;
  end;
end;

theorem Th4:
  for f be non empty FinSequence of NAT, D be disjoint_with_NAT non
  empty set holds signature (FreeUnivAlgNSG(f,D)) = f
proof
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  set fa = FreeUnivAlgNSG(f,D), A = TS DTConUA(f,D);
A1: len the charact of(fa)= len f by Def11;
A2: len(signature fa) = len the charact of(fa) by UNIALG_1:def 4;
  then
A3: dom (signature fa) = Seg len f by A1,FINSEQ_1:def 3;
  now
    let n be Nat;
    reconsider h = FreeOpNSG(n,f,D) as homogeneous quasi_total non empty
    PartFunc of (the carrier of fa)*,(the carrier of fa);
A4: dom h=(arity h)-tuples_on (the carrier of fa) by MARGREL1:22;
    assume
A5: n in dom (signature fa);
    then
A6: n in dom f by A3,FINSEQ_1:def 3;
    then dom h = (f/.n)-tuples_on A by Def10;
    then
A7: arity h = f/.n by A4,FINSEQ_2:110;
    n in dom(FreeOpSeqNSG(f,D)) by A1,A3,A5,FINSEQ_1:def 3;
    then (the charact of fa).n = FreeOpNSG(n,f,D) by Def11;
    hence (signature fa).n = arity h by A5,UNIALG_1:def 4
      .= f.n by A6,A7,PARTFUN1:def 6;
  end;
  hence thesis by A2,A1,FINSEQ_2:9;
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  func FreeGenSetNSG(f,D) -> Subset of FreeUnivAlgNSG(f,D) equals
  {root-tree s
  where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
  coherence
  proof
    set X = DTConUA(f,D), A = {root-tree d where d is Symbol of X: d in
    Terminals X};
    A c= the carrier of FreeUnivAlgNSG(f,D)
    proof
      let x;
      assume x in A;
      then ex d be Symbol of X st x = root-tree d & d in Terminals X;
      hence thesis by DTCONSTR:def 1;
    end;
    hence thesis;
  end;
end;

theorem Th5:
  for f be non empty FinSequence of NAT,D be non empty
  disjoint_with_NAT set holds FreeGenSetNSG(f,D) is non empty
proof
  let f be non empty FinSequence of NAT,D be disjoint_with_NAT non empty set;
  set X = DTConUA(f,D);
  set d = the Element of D;
  reconsider d1 = d as Symbol of X by XBOOLE_0:def 3;
  Terminals X = D by Th3;
  then root-tree d1 in {root-tree k where k is Symbol of X: k in Terminals X};
  hence thesis;
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  redefine func FreeGenSetNSG(f,D) -> GeneratorSet of FreeUnivAlgNSG(f,D);
  coherence
  proof
    set fgs = FreeGenSetNSG(f,D), fua = FreeUnivAlgNSG(f,D);
A1: the carrier of GenUnivAlg(fgs) = the carrier of fua
    proof
      set A = DTConUA(f,D);
      defpred P[DecoratedTree of the carrier of A] means $1 in the carrier of
      GenUnivAlg(fgs);
      the carrier of GenUnivAlg(fgs) is Subset of fua by UNIALG_2:def 7;
      hence the carrier of GenUnivAlg(fgs) c= the carrier of fua;
A2:   for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts & for t being DecoratedTree of the carrier of A st t in rng ts holds P
      [t] holds P[nt-tree ts]
      proof
        reconsider B = the carrier of GenUnivAlg(fgs) as Subset of fua by
UNIALG_2:def 7;
        let s be Symbol of A,p be FinSequence of TS(A);
        assume that
A3:     s ==> roots p and
A4:     for t be DecoratedTree of the carrier of A st t in rng p
        holds t in the carrier of GenUnivAlg(fgs);
        rng p c= the carrier of GenUnivAlg(fgs)
        proof
          let x;
          assume
A5:       x in rng p;
          rng p c= FinTrees(the carrier of A) by FINSEQ_1:def 4;
          then reconsider
          x1 = x as Element of FinTrees(the carrier of A) by A5;
          x1 in the carrier of GenUnivAlg(fgs) by A4,A5;
          hence thesis;
        end;
        then reconsider
        cp = p as FinSequence of the carrier of GenUnivAlg(fgs) by
FINSEQ_1:def 4;
        reconsider tp = p as Element of (TS A)* by FINSEQ_1:def 11;
        [s,roots p] in the Rules of A by A3,LANG1:def 1;
        then reconsider rp = roots p as Element of ((dom f) \/ D)* by
ZFMISC_1:87;
        reconsider s0 = s as Element of ((dom f) \/ D);
A6:     [s0,rp] in REL(f,D) by A3,LANG1:def 1;
        then
A7:     s0 in dom f by Def7;
        then reconsider ns = s as Element of NAT;
A8:     f.s0 = len rp by A6,Def7;
        len FreeOpSeqNSG(f,D) = len f by Def11;
        then
A9:     dom FreeOpSeqNSG(f,D) = Seg len f by FINSEQ_1:def 3
          .= dom f by FINSEQ_1:def 3;
        then (FreeOpSeqNSG(f,D)).ns in rng FreeOpSeqNSG(f,D) by A7,
FUNCT_1:def 3;
        then reconsider o = FreeOpNSG(ns,f,D) as operation of fua by A7,A9
,Def11;
        B is opers_closed by UNIALG_2:def 7;
        then
A10:    B is_closed_on o by UNIALG_2:def 4;
A11:    dom FreeOpNSG(ns,f,D) = (f/.ns)-tuples_on TS(A) by A7,Def10;
        dom o = (arity o)-tuples_on the carrier of fua by MARGREL1:22;
        then
A12:    arity o = f/.ns by A11,FINSEQ_2:110;
        dom (roots p) = dom p by TREES_3:def 18
          .= Seg len p by FINSEQ_1:def 3;
        then
A13:    len p = len rp by FINSEQ_1:def 3
          .= f/.ns by A7,A8,PARTFUN1:def 6;
        then tp in {w where w is Element of (TS A)* : len w = f/.ns};
        then o.cp = Sym(ns,f,D)-tree p by A7,A11,Def10
          .= s-tree p by A7,Def9;
        hence thesis by A10,A13,A12,UNIALG_2:def 3;
      end;
      let x;
      assume
A14:  x in the carrier of fua;
      then reconsider x1 = x as Element of FinTrees(the carrier of A);
A15:  x1 in TS A by A14;
A16:  for s being Symbol of A st s in Terminals A holds P[root-tree s]
      proof
        let s be Symbol of A;
        assume s in Terminals A;
        then
A17:    root-tree s in {root-tree q where q is Symbol of A: q in Terminals A};
        fgs <> {} by Th5;
        then fgs c= the carrier of GenUnivAlg(fgs) by UNIALG_2:def 12;
        hence thesis by A17;
      end;
      for t being DecoratedTree of the carrier of A st t in TS A holds P[
      t] from DTCONSTR:sch 7(A16,A2);
      hence thesis by A15;
    end;
    fgs <> {} by Th5;
    hence thesis by A1,Lm3;
  end;
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set,
  C be non empty set, s be Symbol of (DTConUA(f,D)), F be Function of
  FreeGenSetNSG(f,D),C;
  assume
A1: s in Terminals (DTConUA(f,D));
  func pi(F,s) -> Element of C equals
  :Def14:
  F.(root-tree s);
  coherence
  proof
    root-tree s in (FreeGenSetNSG(f,D)) & dom F=(FreeGenSetNSG(f,D)) by A1,
FUNCT_2:def 1;
    then rng F c= C & F.(root-tree s) in rng F by FUNCT_1:def 3,RELAT_1:def 19;
    hence thesis;
  end;
end;

definition
  let f be non empty FinSequence of NAT, D be set, s be Symbol of (DTConUA(f,D
  ));
  given p be FinSequence such that
A1: s ==> p;
  func @s -> Element of NAT equals
  :Def15:
  s;
  coherence
  proof
    reconsider s0 = s as Element of ((dom f) \/ D);
    set A = DTConUA(f,D);
    [s,p] in the Rules of A by A1,LANG1:def 1;
    then reconsider p0 = p as Element of ((dom f) \/ D)* by ZFMISC_1:87;
    [s0,p0] in REL(f,D) by A1,LANG1:def 1;
    then s0 in dom f by Def7;
    hence thesis;
  end;
end;

theorem Th6:
  for f be non empty FinSequence of NAT,D be non empty
  disjoint_with_NAT set holds FreeGenSetNSG(f,D) is free
proof
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  set fgs = FreeGenSetNSG(f,D), fua = FreeUnivAlgNSG(f,D);
  let U1 be Universal_Algebra;
  assume
A1: fua,U1 are_similar;
  set A = DTConUA(f,D), c1 = the carrier of U1, cf = the carrier of fua;
  let F be Function of fgs,the carrier of U1;
  deffunc F(Symbol of A) = pi(F,$1);
  deffunc G(Symbol of A,FinSequence,set) = (oper(@$1,U1))/.$3;
  consider ff being Function of TS(A), c1 such that
A2: for t being Symbol of A st t in Terminals A holds ff.(root-tree t) =
  F(t) and
A3: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
  roots ts holds ff.(nt-tree ts) = G(nt,roots ts,ff * ts) from DTCONSTR:sch 8;
  reconsider ff as Function of fua,U1;
  take ff;
  for n being Element of NAT st n in dom the charact of(fua) for o1 be
operation of fua, o2 be operation of U1 st o1=(the charact of fua).n & o2=(the
  charact of U1).n for x be FinSequence of fua st x in dom o1 holds ff.(o1.x) =
  o2.(ff*x)
  proof
A4: Seg len the charact of U1 = dom the charact of U1 by FINSEQ_1:def 3;
    let n be Element of NAT;
    assume
A5: n in dom the charact of fua;
    let o1 be operation of fua, o2 be operation of U1;
    assume that
A6: o1=(the charact of fua).n and
A7: o2=(the charact of U1).n;
    let x be FinSequence of fua;
    assume
A8: x in dom o1;
    reconsider xa = x as FinSequence of TS(A);
    dom (roots xa) = dom xa by TREES_3:def 18
      .= Seg len xa by FINSEQ_1:def 3;
    then
A9: len (roots xa) = len xa by FINSEQ_1:def 3;
    reconsider xa as FinSequence of FinTrees the carrier of A;
    reconsider rxa = roots xa as FinSequence of ((dom f) \/ D);
    reconsider rxa as Element of ((dom f) \/ D)* by FINSEQ_1:def 11;
    dom o1 = (arity o1)-tuples_on cf by MARGREL1:22
      .= {w where w is Element of cf* : len w = arity o1};
    then
A10: ex w be Element of cf* st x = w & len w = arity o1 by A8;
A11: o1 = FreeOpNSG(n,f,D) by A5,A6,Def11;
    reconsider fx = ff*x as Element of c1*;
A12: dom o2 = (arity o2)-tuples_on c1 by MARGREL1:22
      .= {v where v is Element of c1*: len v = arity o2};
A13: len the charact of(fua) = len the charact of(U1) & Seg len the
    charact of( fua) = dom the charact of(fua) by A1,FINSEQ_1:def 3,UNIALG_2:1;
A14: dom FreeOpSeqNSG(f,D) = Seg len FreeOpSeqNSG(f,D) by FINSEQ_1:def 3;
A15: len FreeOpSeqNSG(f,D) = len f & Seg len f = dom f by Def11,FINSEQ_1:def 3;
    then reconsider nt = n as Symbol of A by A5,A14,XBOOLE_0:def 3;
    reconsider nd = n as Element of ((dom f) \/ D) by A5,A15,A14,XBOOLE_0:def 3
    ;
A16: f = signature fua by Th4;
    then
A17: (signature fua).n = arity o1 by A5,A6,A15,A14,UNIALG_1:def 4;
    then [nd,rxa] in REL(f,D) by A5,A15,A14,A16,A10,A9,Def7;
    then
A18: nt ==> (roots xa) by LANG1:def 1;
    then
A19: ff.(nt-tree xa) = (oper(@nt,U1))/.(ff*x) by A3;
    @nt = n by A18,Def15;
    then
A20: oper(@nt,U1) = o2 by A5,A7,A13,A4,Def3;
    signature fua = signature U1 by A1,UNIALG_2:def 1;
    then len (ff*x) = len x & arity o2 = len x by A5,A7,A15,A14,A16,A10,A17,
FINSEQ_3:120,UNIALG_1:def 4;
    then
A21: fx in {v where v is Element of c1*: len v = arity o2};
    reconsider xa as Element of (TS A)* by FINSEQ_1:def 11;
    Sym(n,f,D) = nt by A5,A15,A14,Def9;
    then o1.x = nt-tree xa by A5,A8,A15,A14,A11,Def10;
    hence thesis by A19,A20,A12,A21,PARTFUN1:def 6;
  end;
  hence ff is_homomorphism fua,U1 by A1,ALG_1:def 1;
A22: (the carrier of fua) /\ fgs = fgs by XBOOLE_1:28;
A23: dom (ff|fgs) = dom ff /\ fgs & dom ff = (the carrier of fua) by
FUNCT_2:def 1,RELAT_1:61;
A24: now
    let x;
    assume
A25: x in dom F;
    then x in {root-tree t where t is Symbol of A: t in Terminals A};
    then consider s be Symbol of A such that
A26: x = root-tree s & s in Terminals A;
    thus (ff|fgs).x = ff.x by A23,A22,A25,FUNCT_1:47
      .= pi(F,s) by A2,A26
      .= F.x by A26,Def14;
  end;
  fgs = dom F by FUNCT_2:def 1;
  hence thesis by A23,A22,A24,FUNCT_1:2;
end;

registration
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  cluster FreeUnivAlgNSG(f,D) -> free;
  coherence
  proof
    FreeGenSetNSG(f,D) is free by Th6;
    hence thesis by Def6;
  end;
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  redefine func FreeGenSetNSG(f,D) -> free GeneratorSet of FreeUnivAlgNSG(f,D);
  coherence by Th6;
end;

begin

::
:: Construction of Free Universal Algebra for Given Signature
::  (with at Last One Zero Argument Operation) and Set of Generators
::

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
  n be Nat;
  assume
A1: n in dom f;
  func FreeOpZAO(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
  DTConUA(f,D))*, TS(DTConUA(f,D)) means
  :Def16:
  dom it = (f/.n)-tuples_on TS(
  DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
  it.p = Sym(n,f,D)-tree(p);
  existence
  proof
    set A = DTConUA(f,D), i = f/.n, Y = (dom f) \/ D, smm = Sym(n,f,D);
    defpred P[set,set] means $1 in i-tuples_on (TS A) & for p be FinSequence
    of (TS A) st p = $1 holds $2 = smm-tree(p);
    set tu = {s where s is Element of (TS A)*: len s = f/.n};
A2: i = f.n by A1,PARTFUN1:def 6;
A3: for x,y st x in (TS A)* & P[x,y] holds y in (TS A)
    proof
      reconsider sm = Sym(n,f,D) as Element of Y;
      let x,y;
      assume that
      x in (TS A)* and
A4:   P[x,y];
      consider s be Element of (TS A)* such that
A5:   s = x and
A6:   len s = i by A4;
A7:   y = Sym(n,f,D)-tree(s) by A4,A5;
      reconsider s as FinSequence of (TS A);
      dom (roots s) = dom s & Seg len (roots s) = dom(roots s) by
FINSEQ_1:def 3,TREES_3:def 18;
      then
A8:   len (roots s) = i by A6,FINSEQ_1:def 3;
      reconsider s as FinSequence of FinTrees the carrier of A;
      reconsider rs = roots s as Element of Y* by FINSEQ_1:def 11;
      sm = n by A1,Def9;
      then [sm,rs] in REL(f,D) by A1,A2,A8,Def7;
      then Sym(n,f,D) ==> roots s by LANG1:def 1;
      hence thesis by A7,DTCONSTR:def 1;
    end;
A9: for x,y1,y2 be set st x in (TS A)* & P[x,y1] & P[x,y2] holds y1 = y2
    proof
      let x,y1,y2 be set;
      assume that
      x in (TS A)* and
A10:  P[x,y1] and
A11:  P[x,y2];
      consider s be Element of (TS A)* such that
A12:  s = x and
      len s = i by A10;
      y1 = Sym(n,f,D)-tree(s) by A10,A12;
      hence thesis by A11,A12;
    end;
    consider F being PartFunc of (TS A)*,(TS A) such that
A13: for x be set holds x in dom F iff x in (TS A)* & ex y st P[x,y] and
A14: for x be set st x in dom F holds P[x,F.x] from PARTFUN1:sch 2(A3,
    A9);
A15: dom F = i-tuples_on (TS A)
    proof
      thus dom F c= i-tuples_on(TS A)
      proof
        let x;
        assume x in dom F;
        then ex y st P[x,y] by A13;
        hence thesis;
      end;
      reconsider sm = smm as Symbol of A;
      let x;
      assume x in i-tuples_on(TS A);
      then consider s be Element of (TS A)* such that
A16:  s = x and
A17:  len s = i;
      P[s,sm-tree(s)] by A17;
      hence thesis by A13,A16;
    end;
A18: for x,y be FinSequence of TS(A) st len x=len y & x in dom F holds y
    in dom F
    proof
      let x,y be FinSequence of TS(A);
      assume that
A19:  len x = len y and
A20:  x in dom F;
      reconsider sy = y as Element of (TS A)* by FINSEQ_1:def 11;
      ex sx be Element of (TS A)* st sx = x & len sx = f/.n by A15,A20;
      then sy in tu by A19;
      hence thesis by A15;
    end;
A21:  ex x being FinSequence st x in dom F
    proof
      set a = the Element of i-tuples_on(TS A);
      a in dom F by A15;
      hence ex x being FinSequence st x in dom F;
    end;
    dom F is with_common_domain
    proof
      let x,y be FinSequence;
      assume x in dom F & y in dom F;
      then (ex sx be Element of (TS A)* st sx = x & len sx = f/.n )& ex sy be
      Element of (TS A)* st sy = y & len sy = f/.n by A15;
      hence thesis;
    end;
    then reconsider
    F as homogeneous quasi_total non empty PartFunc of (TS A)*, TS(
    A) by A18,A21,MARGREL1:def 21,def 22;
    take F;
    thus dom F = i-tuples_on (TS A) by A15;
    let p be FinSequence of (TS A);
    assume p in dom F;
    hence thesis by A14;
  end;
  uniqueness
  proof
    set A = TS DTConUA(f,D);
    let f1,f2 be homogeneous quasi_total non empty PartFunc of A*,A;
    assume that
A22: dom f1 = (f/.n)-tuples_on A and
A23: for p be FinSequence of A st p in dom f1 holds f1.p = Sym(n,f,D)
    -tree(p) and
A24: dom f2 = (f/.n)-tuples_on A and
A25: for p be FinSequence of A st p in dom f2 holds f2.p = Sym(n,f,D) -tree(p);
    now
      let x;
      assume
A26:  x in (f/.n)-tuples_on A;
      then consider s be Element of A* such that
A27:  s = x and
      len s = f/.n;
      f1.s = Sym(n,f,D)-tree(s) by A22,A23,A26,A27;
      hence f1.x = f2.x by A24,A25,A26,A27;
    end;
    hence thesis by A22,A24,FUNCT_1:2;
  end;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeOpSeqZAO(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
  :Def17:
  len it = len f & for n st n in dom it holds it.n = FreeOpZAO(n,f,D);
  existence
  proof
    defpred P[Nat,set] means $2 = FreeOpZAO($1,f,D);
    set A = TS(DTConUA(f,D));
A1: for n be Nat st n in Seg len f ex x be Element of PFuncs(A*,A) st P[n, x]
    proof
      let n be Nat;
      assume n in Seg len f;
      reconsider O=FreeOpZAO(n,f,D) as Element of PFuncs(A*,A) by PARTFUN1:45;
      take O;
      thus thesis;
    end;
    consider p be FinSequence of PFuncs(A*,A) such that
A2: dom p = Seg len f & for n be Nat st n in Seg len f holds P[n,p.n]
    from FINSEQ_1:sch 5(A1);
    reconsider p as PFuncFinSequence of A;
    take p;
    thus len p = len f by A2,FINSEQ_1:def 3;
    let n;
    assume n in dom p;
    hence thesis by A2;
  end;
  uniqueness
  proof
    let f1,f2 be PFuncFinSequence of TS DTConUA(f,D);
    assume that
A3: len f1 = len f and
A4: for n st n in dom f1 holds f1.n = FreeOpZAO(n,f,D) and
A5: len f2 = len f and
A6: for n st n in dom f2 holds f2.n = FreeOpZAO(n,f,D);
A7: dom f1 = Seg len f1 by FINSEQ_1:def 3;
A8: dom f = Seg len f by FINSEQ_1:def 3;
A9: dom f2 = Seg len f2 by FINSEQ_1:def 3;
    for n being Nat st n in dom f holds f1.n = f2.n
    proof
      let n be Nat;
      assume
A10:  n in dom f;
      then f1.n = FreeOpZAO(n,f,D) by A3,A4,A8,A7;
      hence thesis by A5,A6,A8,A9,A10;
    end;
    hence thesis by A3,A5,A8,A7,FINSEQ_2:9;
  end;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeUnivAlgZAO(f,D) -> strict Universal_Algebra equals
  UAStr (# TS(
    DTConUA(f,D)), FreeOpSeqZAO(f,D)#);
  coherence
  proof
    set A = TS DTConUA(f,D), AA = UAStr (# A, FreeOpSeqZAO(f,D) #);
    for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
    = (the charact of AA).n holds h is quasi_total
    proof
      let n be Nat,h be PartFunc of A*,A;
      assume n in dom the charact of(AA) & h = (the charact of AA).n;
      then h = FreeOpZAO(n,f,D) by Def17;
      hence thesis;
    end;
    then
A1: the charact of(AA) is quasi_total by MARGREL1:def 24;
    for n be Nat,h be PartFunc of A*,A st n in dom the charact of(AA) & h
    = (the charact of AA).n holds h is homogeneous
    proof
      let n be Nat,h be PartFunc of A*,A;
      assume n in dom the charact of(AA) & h = (the charact of AA).n;
      then h = FreeOpZAO(n,f,D) by Def17;
      hence thesis;
    end;
    then
A2: the charact of(AA) is homogeneous by MARGREL1:def 23;
    for n be set st n in dom the charact of(AA) holds (the charact of AA)
    .n is non empty
    proof
      let n be set;
      assume
A3:   n in dom the charact of AA;
      then reconsider n as Element of NAT;
      (the charact of AA).n = FreeOpZAO(n,f,D) by A3,Def17;
      hence thesis;
    end;
    then
A4: the charact of AA is non-empty by FUNCT_1:def 9;
    len FreeOpSeqZAO(f,D) = len f by Def17;
    then the charact of AA <> {};
    hence thesis by A1,A2,A4,UNIALG_1:def 1,def 2,def 3;
  end;
end;

theorem Th7:
  for f be with_zero non empty FinSequence of NAT, D be
  disjoint_with_NAT set holds signature (FreeUnivAlgZAO(f,D)) = f
proof
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  set fa = FreeUnivAlgZAO(f,D), A = TS DTConUA(f,D);
A1: len the charact of fa = len f by Def17;
A2: len(signature fa) = len the charact of(fa) by UNIALG_1:def 4;
  then
A3: dom(signature fa) = Seg len f by A1,FINSEQ_1:def 3;
  now
    let n be Nat;
    reconsider h = FreeOpZAO(n,f,D) as homogeneous quasi_total non empty
    PartFunc of (the carrier of fa)*,(the carrier of fa);
A4: dom h = (arity h)-tuples_on (the carrier of fa) by MARGREL1:22;
    assume
A5: n in dom(signature fa);
    then
A6: n in dom f by A3,FINSEQ_1:def 3;
    then dom h = (f/.n)-tuples_on A by Def16;
    then
A7: arity h = f/.n by A4,FINSEQ_2:110;
    n in dom(FreeOpSeqZAO(f,D)) by A1,A3,A5,FINSEQ_1:def 3;
    then (the charact of fa).n = FreeOpZAO(n,f,D) by Def17;
    hence (signature fa).n = arity h by A5,UNIALG_1:def 4
      .= f.n by A6,A7,PARTFUN1:def 6;
  end;
  hence thesis by A2,A1,FINSEQ_2:9;
end;

theorem Th8:
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds FreeUnivAlgZAO(f,D) is with_const_op
proof
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  set A = DTConUA(f,D), AA = FreeUnivAlgZAO(f,D);
A1: dom f = Seg len f by FINSEQ_1:def 3;
  0 in rng f by Def2;
  then consider n being Nat such that
A2: n in dom f and
A3: f.n = 0 by FINSEQ_2:10;
A4: len FreeOpSeqZAO(f,D) = len f & dom FreeOpSeqZAO(f,D) = Seg len
  FreeOpSeqZAO (f,D) by Def17,FINSEQ_1:def 3;
  then (the charact of AA).n = FreeOpZAO(n,f,D) by A2,A1,Def17;
  then reconsider o = FreeOpZAO(n,f,D) as operation of AA by A2,A4,A1,
FUNCT_1:def 3;
  take o;
A5: dom o = (arity o)-tuples_on (the carrier of AA) by MARGREL1:22;
  f/.n = f.n & dom(FreeOpZAO(n,f,D)) = (f/.n)-tuples_on (TS A) by A2,Def16,
PARTFUN1:def 6;
  hence thesis by A3,A5,FINSEQ_2:110;
end;

theorem Th9:
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds Constants(FreeUnivAlgZAO(f,D)) <> {}
proof
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  set A = DTConUA(f,D), AA = FreeUnivAlgZAO(f,D);
A1: dom f = Seg len f by FINSEQ_1:def 3;
  set ca = the carrier of AA;
  0 in rng f by Def2;
  then consider n being Nat such that
A2: n in dom f and
A3: f.n = 0 by FINSEQ_2:10;
A4: len FreeOpSeqZAO(f,D) = len f & dom FreeOpSeqZAO(f,D) = Seg len
  FreeOpSeqZAO (f,D) by Def17,FINSEQ_1:def 3;
  then (the charact of AA).n = FreeOpZAO(n,f,D) by A2,A1,Def17;
  then reconsider o = FreeOpZAO(n,f,D) as operation of AA by A2,A4,A1,
FUNCT_1:def 3;
A5: f/.n = f.n & dom(FreeOpZAO(n,f,D)) = (f/.n)-tuples_on (TS A) by A2,Def16,
PARTFUN1:def 6;
  then dom o = {<*>(TS A)} by A3,FINSEQ_2:94;
  then <*>(TS A) in dom o by TARSKI:def 1;
  then
A6: o.(<*>(TS A)) in rng o by FUNCT_1:def 3;
  rng o c= ca by RELAT_1:def 19;
  then reconsider e = o.(<*>(TS A)) as Element of ca by A6;
  dom o = (arity o)-tuples_on (the carrier of AA) by MARGREL1:22;
  then arity o = 0 by A3,A5,FINSEQ_2:110;
  then e in {a where a is Element of ca: ex o be operation of AA st arity o =
  0 & a in rng o} by A6;
  hence thesis;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeGenSetZAO(f,D) -> Subset of FreeUnivAlgZAO(f,D) equals
  {root-tree s
  where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
  coherence
  proof
    set X = DTConUA(f,D), A = {root-tree d where d is Symbol of X: d in
    Terminals X};
    A c= the carrier of FreeUnivAlgZAO(f,D)
    proof
      let x;
      assume x in A;
      then ex d be Symbol of X st x = root-tree d & d in Terminals X;
      hence thesis by DTCONSTR:def 1;
    end;
    hence thesis;
  end;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  redefine func FreeGenSetZAO(f,D) -> GeneratorSet of FreeUnivAlgZAO(f,D);
  coherence
  proof
    set fgs = FreeGenSetZAO(f,D), fua = FreeUnivAlgZAO(f,D);
A1: the carrier of GenUnivAlg(fgs) = the carrier of fua
    proof
      set A = DTConUA(f,D);
      defpred P[DecoratedTree of the carrier of A] means $1 in the carrier of
      GenUnivAlg(fgs);
      the carrier of GenUnivAlg(fgs) is Subset of fua by UNIALG_2:def 7;
      hence the carrier of GenUnivAlg(fgs) c= the carrier of fua;
A2:   for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
roots ts & for t being DecoratedTree of the carrier of A st t in rng ts holds P
      [t] holds P[nt-tree ts]
      proof
        reconsider B = the carrier of GenUnivAlg(fgs) as Subset of fua by
UNIALG_2:def 7;
        let s be Symbol of A,p be FinSequence of TS(A);
        assume that
A3:     s ==> roots p and
A4:     for t be DecoratedTree of the carrier of A st t in rng p
        holds t in the carrier of GenUnivAlg(fgs);
        rng p c= the carrier of GenUnivAlg(fgs)
        proof
          let x;
          assume
A5:       x in rng p;
          rng p c= FinTrees(the carrier of A) by FINSEQ_1:def 4;
          then reconsider
          x1 = x as Element of FinTrees(the carrier of A) by A5;
          x1 in the carrier of GenUnivAlg(fgs) by A4,A5;
          hence thesis;
        end;
        then reconsider
        cp = p as FinSequence of the carrier of GenUnivAlg(fgs) by
FINSEQ_1:def 4;
        reconsider tp = p as Element of (TS A)* by FINSEQ_1:def 11;
        [s,roots p] in the Rules of A by A3,LANG1:def 1;
        then reconsider rp = roots p as Element of ((dom f) \/ D)* by
ZFMISC_1:87;
        reconsider s0 = s as Element of ((dom f) \/ D);
A6:     [s0,rp] in REL(f,D) by A3,LANG1:def 1;
        then
A7:     s0 in dom f by Def7;
        then reconsider ns = s as Element of NAT;
A8:     f.s0 = len rp by A6,Def7;
        len FreeOpSeqZAO(f,D) = len f by Def17;
        then
A9:     dom FreeOpSeqZAO(f,D) = Seg len f by FINSEQ_1:def 3
          .= dom f by FINSEQ_1:def 3;
        then (FreeOpSeqZAO(f,D)).ns in rng FreeOpSeqZAO(f,D) by A7,
FUNCT_1:def 3;
        then reconsider o = FreeOpZAO(ns,f,D) as operation of fua by A7,A9
,Def17;
        B is opers_closed by UNIALG_2:def 7;
        then
A10:    B is_closed_on o by UNIALG_2:def 4;
A11:    dom FreeOpZAO(ns,f,D) = (f/.ns)-tuples_on TS(A) by A7,Def16;
        dom o = (arity o)-tuples_on the carrier of fua by MARGREL1:22;
        then
A12:    arity o = f/.ns by A11,FINSEQ_2:110;
        dom (roots p) = dom p by TREES_3:def 18
          .= Seg len p by FINSEQ_1:def 3;
        then
A13:    len p = len rp by FINSEQ_1:def 3
          .= f/.ns by A7,A8,PARTFUN1:def 6;
        then tp in {w where w is Element of (TS A)* : len w = f/.ns};
        then o.cp = Sym(ns,f,D)-tree p by A7,A11,Def16
          .= s-tree p by A7,Def9;
        hence thesis by A10,A13,A12,UNIALG_2:def 3;
      end;
      let x;
      assume
A14:  x in the carrier of fua;
      then reconsider x1 = x as Element of FinTrees(the carrier of A);
A15:  x1 in TS A by A14;
A16:  for s being Symbol of A st s in Terminals A holds P[root-tree s]
      proof
        let s be Symbol of A;
        assume s in Terminals A;
        then
A17:    root-tree s in {root-tree q where q is Symbol of A: q in Terminals A};
        Constants(fua) <> {} by Th9;
        then fgs c= the carrier of GenUnivAlg(fgs) by UNIALG_2:def 12;
        hence thesis by A17;
      end;
      for t being DecoratedTree of the carrier of A st t in TS A holds P[
      t] from DTCONSTR:sch 7(A16,A2);
      hence thesis by A15;
    end;
    Constants(fua) <> {} by Th9;
    hence thesis by A1,Lm3;
  end;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
  C be non empty set, s be Symbol of (DTConUA(f,D)), F be Function of (
  FreeGenSetZAO(f,D)),C;
  assume
A1: s in Terminals (DTConUA(f,D));
  func pi(F,s) -> Element of C equals
  :Def20:
  F.(root-tree s);
  coherence
  proof
    root-tree s in (FreeGenSetZAO(f,D)) & dom F=(FreeGenSetZAO(f,D)) by A1,
FUNCT_2:def 1;
    then rng F c= C & F.(root-tree s) in rng F by FUNCT_1:def 3,RELAT_1:def 19;
    hence thesis;
  end;
end;

theorem Th10:
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds FreeGenSetZAO(f,D) is free
proof
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  set fgs = FreeGenSetZAO(f,D), fua = FreeUnivAlgZAO(f,D);
  let U1 be Universal_Algebra;
  assume
A1: fua,U1 are_similar;
  set A = DTConUA(f,D), c1 = the carrier of U1, cf = the carrier of fua;
  let F be Function of fgs,the carrier of U1;
  deffunc F(Symbol of A) = pi(F,$1);
  deffunc G(Symbol of A,FinSequence,set) = (oper(@$1,U1))/.$3;
  consider ff being Function of TS(A), c1 such that
A2: for t being Symbol of A st t in Terminals A holds ff.(root-tree t) =
  F(t) and
A3: for nt being Symbol of A, ts being FinSequence of TS(A) st nt ==>
  roots ts holds ff.(nt-tree ts) = G(nt,roots ts,ff * ts) from DTCONSTR:sch 8;
  reconsider ff as Function of fua,U1;
  take ff;
  for n being Element of NAT st n in dom the charact of(fua) for o1 be
operation of fua, o2 be operation of U1 st o1=(the charact of fua).n & o2=(the
  charact of U1).n for x be FinSequence of fua st x in dom o1 holds ff.(o1.x) =
  o2.(ff*x)
  proof
A4: dom the charact of(U1) = Seg len the charact of(U1) by FINSEQ_1:def 3;
    let n be Element of NAT;
    assume
A5: n in dom the charact of(fua);
    let o1 be operation of fua, o2 be operation of U1;
    assume that
A6: o1=(the charact of fua).n and
A7: o2=(the charact of U1).n;
    let x be FinSequence of fua;
    assume
A8: x in dom o1;
    reconsider xa = x as FinSequence of TS(A);
    dom (roots xa) = dom xa by TREES_3:def 18
      .= Seg len xa by FINSEQ_1:def 3;
    then
A9: len (roots xa) = len xa by FINSEQ_1:def 3;
    reconsider xa as FinSequence of FinTrees the carrier of A;
    reconsider rxa = roots xa as FinSequence of ((dom f) \/ D);
    reconsider rxa as Element of ((dom f) \/ D)* by FINSEQ_1:def 11;
    dom o1 = (arity o1)-tuples_on cf by MARGREL1:22
      .= {w where w is Element of cf* : len w = arity o1};
    then
A10: ex w be Element of cf* st x = w & len w = arity o1 by A8;
A11: o1 = FreeOpZAO(n,f,D) by A5,A6,Def17;
    reconsider fx = ff*x as Element of c1*;
A12: dom o2 = (arity o2)-tuples_on c1 by MARGREL1:22
      .= {v where v is Element of c1*: len v = arity o2};
A13: len the charact of(fua) = len the charact of(U1) & dom the charact of
    (fua) = Seg len the charact of(fua) by A1,FINSEQ_1:def 3,UNIALG_2:1;
A14: Seg len FreeOpSeqZAO(f,D) = dom FreeOpSeqZAO(f,D) by FINSEQ_1:def 3;
A15: len FreeOpSeqZAO(f,D) = len f & dom f = Seg len f by Def17,FINSEQ_1:def 3;
    then reconsider nt = n as Symbol of A by A5,A14,XBOOLE_0:def 3;
    reconsider nd = n as Element of ((dom f) \/ D) by A5,A15,A14,XBOOLE_0:def 3
    ;
A16: f = signature fua by Th7;
    then
A17: (signature fua).n = arity o1 by A5,A6,A15,A14,UNIALG_1:def 4;
    then [nd,rxa] in REL(f,D) by A5,A15,A14,A16,A10,A9,Def7;
    then
A18: nt ==> (roots xa) by LANG1:def 1;
    then
A19: ff.(nt-tree xa) = (oper(@nt,U1))/.(ff*x) by A3;
    @nt = n by A18,Def15;
    then
A20: oper(@nt,U1) = o2 by A5,A7,A13,A4,Def3;
    signature fua = signature U1 by A1,UNIALG_2:def 1;
    then len (ff*x) = len x & arity o2 = len x by A5,A7,A15,A14,A16,A10,A17,
FINSEQ_3:120,UNIALG_1:def 4;
    then
A21: fx in {v where v is Element of c1*: len v = arity o2};
    reconsider xa as Element of (TS A)* by FINSEQ_1:def 11;
    Sym(n,f,D) = nt by A5,A15,A14,Def9;
    then o1.x = nt-tree xa by A5,A8,A15,A14,A11,Def16;
    hence thesis by A19,A20,A12,A21,PARTFUN1:def 6;
  end;
  hence ff is_homomorphism fua,U1 by A1,ALG_1:def 1;
A22: (the carrier of fua) /\ fgs = fgs by XBOOLE_1:28;
A23: dom (ff|fgs) = dom ff /\ fgs & dom ff = (the carrier of fua) by
FUNCT_2:def 1,RELAT_1:61;
A24: now
    let x;
    assume
A25: x in dom F;
    then x in {root-tree t where t is Symbol of A: t in Terminals A};
    then consider s be Symbol of A such that
A26: x = root-tree s & s in Terminals A;
    thus (ff|fgs).x = ff.x by A23,A22,A25,FUNCT_1:47
      .= pi(F,s) by A2,A26
      .= F.x by A26,Def20;
  end;
  fgs = dom F by FUNCT_2:def 1;
  hence thesis by A23,A22,A24,FUNCT_1:2;
end;

registration
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  cluster FreeUnivAlgZAO(f,D) -> free;
  coherence
  proof
    FreeGenSetZAO(f,D) is free by Th10;
    hence thesis by Def6;
  end;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  redefine func FreeGenSetZAO(f,D) -> free GeneratorSet of FreeUnivAlgZAO(f,D);
  coherence by Th10;
end;

registration
  cluster strict free with_const_op for Universal_Algebra;
  existence
  proof
    set D = the disjoint_with_NAT set;
    set f = the with_zero non empty FinSequence of NAT;
    take FreeUnivAlgZAO(f,D);
    thus thesis by Th8;
  end;
end;