freealg.miz



    begin

    reserve x,y for set,

n for Nat;

    definition

      let IT be set;

      :: FREEALG:def1

      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 be object such that

           A1: x in X and

           A2: x in NAT by XBOOLE_0: 3;

          reconsider x as Nat by A2;

          x = ( - 1) by A1, TARSKI:def 1;

          hence contradiction by NAT_1: 2;

        end;

        hence thesis;

      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;

      :: original: with_zero

      redefine

      :: FREEALG:def2

      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

    definition

      let U1 be Universal_Algebra, n be Nat;

      assume

       A1: n in ( dom the charact of U1);

      :: FREEALG:def3

      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;

      :: FREEALG:def4

      mode GeneratorSet of U0 -> Subset of U0 means for A be 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;

      end;

    end

    

     Lm2: for A be Universal_Algebra holds for B be 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 object;

      assume x in ( Constants A);

      then

      consider a be Element of A such that

       A2: x = a and

       A3: ex o be Element of ( Operations A) st ( arity o) = 0 & a in ( rng o);

      consider o be 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;

      consider s be object 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;

      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;

    end;

    

     Lm3: for A be Universal_Algebra holds for B be 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 be 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 UNIALG_2:def 7, UNIALG_2: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;

      :: FREEALG:def5

      attr IT is free means for U1 be Universal_Algebra st (U0,U1) are_similar holds for f be Function of IT, the carrier of U1 holds ex h be Function of U0, U1 st h is_homomorphism & (h | IT) = f;

    end

    definition

      let IT be Universal_Algebra;

      :: FREEALG:def6

      attr IT is free means

      : Def6: ex G be 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, UNIALG_1:def 2, UNIALG_1:def 3;

        

         A4: ( dom the charact of U0) = {1} by A3, FINSEQ_1: 2, FINSEQ_1: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 be 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);

            ( len the charact of U1) = 1 by A3, A14, UNIALG_2: 1;

            then ( dom the charact of U1) = {1} by FINSEQ_1: 2, FINSEQ_1: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 object 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 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 by A14, ALG_1:def 1;

            f = {} ;

            hence (h | G) = f;

          end;

          hence G is free;

        end;

        hence thesis;

      end;

    end

    registration

      let U0 be free Universal_Algebra;

      cluster free for GeneratorSet of U0;

      existence by Def6;

    end

    theorem :: FREEALG:1

    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

    definition

      let f be non empty FinSequence of NAT , X be set;

      :: FREEALG:def7

      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 be Relation of A, (A * ) such that

         A1: for x be Element of A, y be 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 be object holds [x, y] in R iff [x, y] in T

        proof

          let x,y be object;

          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;

      :: FREEALG:def8

      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 :: FREEALG:2

    

     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)) = {} ;

      thus ( Terminals A) c= X

      proof

        let x be object;

        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 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 be 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 be object;

        assume x in ( NonTerminals A);

        then x in { t where t be 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 be object;

      

       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 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 be Symbol of A : ex n be FinSequence st t ==> n };

      hence thesis by LANG1:def 3;

    end;

    theorem :: FREEALG:3

    

     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 be object;

      assume

       A1: x in X;

      

       A2: ( NonTerminals A) = ( dom f) by Th2;

      

       A3: not x in ( NonTerminals A) by A2, A1, Def1, XBOOLE_0: 3;

      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 by Th2;

    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 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 be object 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 be object;

            assume y in ( rng p);

            then

             A9: ex n be 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 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 be object;

            assume y in ( rng p);

            then

            consider n be 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;

      end;

    end

    definition

      let f be non empty FinSequence of NAT , X be set, n be Nat;

      assume

       A1: n in ( dom f);

      :: FREEALG:def9

      func Sym (n,f,X) -> Symbol of ( DTConUA (f,X)) equals

      : Def9: n;

      coherence by A1, XBOOLE_0:def 3;

    end

    begin

    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);

      :: FREEALG:def10

      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[ object, object] 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 be Element of (( TS A) * ) : ( len s) = (f /. n) };

        

         A2: i = (f . n) by A1, PARTFUN1:def 6;

        

         A3: for x,y be object 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 be object;

          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 object st x in (( TS A) * ) & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object;

          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 be PartFunc of (( TS A) * ), ( TS A) such that

         A13: for x be object holds x in ( dom F) iff x in (( TS A) * ) & ex y be object st P[x, y] and

         A14: for x be object 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 be object;

            assume x in ( dom F);

            then ex y be object st P[x, y] by A13;

            hence thesis;

          end;

          reconsider sm = smm as Symbol of A;

          let x be object;

          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 be 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 be 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, MARGREL1: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 be object;

          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;

      :: FREEALG:def11

      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)) holds 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 be 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;

      :: FREEALG:def12

      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;

        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;

        for n be object st n in ( dom the charact of AA) holds (the charact of AA . n) is non empty

        proof

          let n be object;

          assume

           A3: n in ( dom the charact of AA);

          then

          reconsider n as 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, UNIALG_1:def 2, UNIALG_1:def 3;

      end;

    end

    theorem :: FREEALG:4

    

     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;

      :: FREEALG:def13

      func FreeGenSetNSG (f,D) -> Subset of ( FreeUnivAlgNSG (f,D)) equals { ( root-tree s) where s be Symbol of ( DTConUA (f,D)) : s in ( Terminals ( DTConUA (f,D))) };

      coherence

      proof

        set X = ( DTConUA (f,D)), A = { ( root-tree d) where d be Symbol of X : d in ( Terminals X) };

        A c= the carrier of ( FreeUnivAlgNSG (f,D))

        proof

          let x be object;

          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 :: FREEALG:5

    

     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 be 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;

      :: original: FreeGenSetNSG

      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 be Symbol of A, ts be FinSequence of ( TS A) st nt ==> ( roots ts) & for t be 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 be object;

              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 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;

            

             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 be 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;

          end;

          let x be object;

          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 be 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 be Symbol of A : q in ( Terminals A) };

            fgs c= the carrier of ( GenUnivAlg fgs) by UNIALG_2:def 12;

            hence thesis by A17;

          end;

          for t be 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)));

      :: FREEALG:def14

      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;

      :: FREEALG:def15

      func @ s -> 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 :: FREEALG:6

    

     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 be Function of ( TS A), c1 such that

       A2: for t be Symbol of A st t in ( Terminals A) holds (ff . ( root-tree t)) = F(t) and

       A3: for nt be Symbol of A, ts be FinSequence of ( TS A) st nt ==> ( roots ts) holds (ff . (nt -tree ts)) = G(nt,roots,*) from DTCONSTR:sch 8;

      reconsider ff as Function of fua, U1;

      take ff;

      for n be Nat st n in ( dom the charact of fua) holds for o1 be operation of fua, o2 be operation of U1 st o1 = (the charact of fua . n) & o2 = (the charact of U1 . n) holds 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 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 be 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 be 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;

        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 be 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 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 be object;

        assume

         A25: x in ( dom F);

        then x in { ( root-tree t) where t be 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;

      end;

    end

    definition

      let f be non empty FinSequence of NAT , D be non empty disjoint_with_NAT set;

      :: original: FreeGenSetNSG

      redefine

      func FreeGenSetNSG (f,D) -> free GeneratorSet of ( FreeUnivAlgNSG (f,D)) ;

      coherence by Th6;

    end

    begin

    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);

      :: FREEALG:def16

      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[ object, object] 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 be Element of (( TS A) * ) : ( len s) = (f /. n) };

        

         A2: i = (f . n) by A1, PARTFUN1:def 6;

        

         A3: for x,y be object 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 be object;

          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 object st x in (( TS A) * ) & P[x, y1] & P[x, y2] holds y1 = y2

        proof

          let x,y1,y2 be object;

          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 be PartFunc of (( TS A) * ), ( TS A) such that

         A13: for x be object holds x in ( dom F) iff x in (( TS A) * ) & ex y be object st P[x, y] and

         A14: for x be object 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 be object;

            assume x in ( dom F);

            then ex y be object st P[x, y] by A13;

            hence thesis;

          end;

          reconsider sm = smm as Symbol of A;

          let x be object;

          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 be 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 be 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, MARGREL1: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 be object;

          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;

      :: FREEALG:def17

      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)) holds 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 be 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;

      :: FREEALG:def18

      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;

        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;

        for n be object st n in ( dom the charact of AA) holds (the charact of AA . n) is non empty

        proof

          let n be object;

          assume

           A3: n in ( dom the charact of AA);

          then

          reconsider n as 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, UNIALG_1:def 2, UNIALG_1:def 3;

      end;

    end

    theorem :: FREEALG:7

    

     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 :: FREEALG:8

    

     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 be 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 :: FREEALG:9

    

     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 be 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 be 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;

      :: FREEALG:def19

      func FreeGenSetZAO (f,D) -> Subset of ( FreeUnivAlgZAO (f,D)) equals { ( root-tree s) where s be Symbol of ( DTConUA (f,D)) : s in ( Terminals ( DTConUA (f,D))) };

      coherence

      proof

        set X = ( DTConUA (f,D)), A = { ( root-tree d) where d be Symbol of X : d in ( Terminals X) };

        A c= the carrier of ( FreeUnivAlgZAO (f,D))

        proof

          let x be object;

          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;

      :: original: FreeGenSetZAO

      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 be Symbol of A, ts be FinSequence of ( TS A) st nt ==> ( roots ts) & for t be 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 be object;

              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 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;

            

             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 be 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;

          end;

          let x be object;

          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 be 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 be Symbol of A : q in ( Terminals A) };

            fgs c= the carrier of ( GenUnivAlg fgs) by UNIALG_2:def 12;

            hence thesis by A17;

          end;

          for t be 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)));

      :: FREEALG:def20

      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 :: FREEALG:10

    

     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 be Function of ( TS A), c1 such that

       A2: for t be Symbol of A st t in ( Terminals A) holds (ff . ( root-tree t)) = F(t) and

       A3: for nt be Symbol of A, ts be FinSequence of ( TS A) st nt ==> ( roots ts) holds (ff . (nt -tree ts)) = G(nt,roots,*) from DTCONSTR:sch 8;

      reconsider ff as Function of fua, U1;

      take ff;

      for n be Nat st n in ( dom the charact of fua) holds for o1 be operation of fua, o2 be operation of U1 st o1 = (the charact of fua . n) & o2 = (the charact of U1 . n) holds 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 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 be 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 be 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;

        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 be 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 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 be object;

        assume

         A25: x in ( dom F);

        then x in { ( root-tree t) where t be 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;

      end;

    end

    definition

      let f be with_zero non empty FinSequence of NAT , D be disjoint_with_NAT set;

      :: original: FreeGenSetZAO

      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