msafree1.miz



    begin

    theorem :: MSAFREE1:1

    

     Th1: for f,g be Function st g in ( product f) holds ( rng g) c= ( Union f)

    proof

      let f,g be Function;

      assume

       A1: g in ( product f);

      let y be object;

      assume y in ( rng g);

      then

      consider x be object such that

       A2: x in ( dom g) and

       A3: y = (g . x) by FUNCT_1:def 3;

      

       A4: ( dom g) = ( dom f) by A1, CARD_3: 9;

      then y in (f . x) by A1, A2, A3, CARD_3: 9;

      hence thesis by A4, A2, CARD_5: 2;

    end;

    scheme :: MSAFREE1:sch1

    DTConstrUniq { DT() -> non empty DTConstrStr , D() -> non empty set , G( set) -> Element of D() , H( set, set, set) -> Element of D() , f1,f2() -> Function of ( TS DT()), D() } :

f1() = f2()

      provided

       A1: for t be Symbol of DT() st t in ( Terminals DT()) holds (f1() . ( root-tree t)) = G(t)

       and

       A2: for nt be Symbol of DT(), ts be Element of (( TS DT()) * ) st nt ==> ( roots ts) holds for x be Element of (D() * ) st x = (f1() * ts) holds (f1() . (nt -tree ts)) = H(nt,ts,x)

       and

       A3: for t be Symbol of DT() st t in ( Terminals DT()) holds (f2() . ( root-tree t)) = G(t)

       and

       A4: for nt be Symbol of DT(), ts be Element of (( TS DT()) * ) st nt ==> ( roots ts) holds for x be Element of (D() * ) st x = (f2() * ts) holds (f2() . (nt -tree ts)) = H(nt,ts,x);

      defpred P[ set] means (f1() . $1) = (f2() . $1);

      

       A5: for nt be Symbol of DT(), ts be FinSequence of ( TS DT()) st nt ==> ( roots ts) & for t be DecoratedTree of the carrier of DT() st t in ( rng ts) holds P[t] holds P[(nt -tree ts)]

      proof

        let nt be Symbol of DT(), ts be FinSequence of ( TS DT());

        assume that

         A6: nt ==> ( roots ts) and

         A7: for t be DecoratedTree of the carrier of DT() st t in ( rng ts) holds (f1() . t) = (f2() . t);

        

         A8: ( rng ts) c= ( TS DT()) by FINSEQ_1:def 4;

        then

         A9: ( rng ts) c= ( dom f1()) by FUNCT_2:def 1;

        then

         A10: ( dom (f1() * ts)) = ( dom ts) by RELAT_1: 27;

        ( rng ts) c= ( dom f2()) by A8, FUNCT_2:def 1;

        then

         A11: ( dom (f2() * ts)) = ( dom ts) by RELAT_1: 27;

         A12:

        now

          let x be object;

          assume

           A13: x in ( dom ts);

          then

          reconsider t = (ts . x) as Element of ( FinTrees the carrier of DT()) by DTCONSTR: 2;

          t in ( rng ts) by A13, FUNCT_1:def 3;

          then

           A14: (f1() . t) = (f2() . t) by A7;

          

          thus ((f1() * ts) . x) = (f1() . t) by A10, A13, FUNCT_1: 12

          .= ((f2() * ts) . x) by A11, A13, A14, FUNCT_1: 12;

        end;

        ( dom (f1() * ts)) = ( dom ts) by A9, RELAT_1: 27

        .= ( Seg ( len ts)) by FINSEQ_1:def 3;

        then

        reconsider ntv1 = (f1() * ts) as FinSequence by FINSEQ_1:def 2;

        ( rng ntv1) c= D() by RELAT_1:def 19;

        then ntv1 is FinSequence of D() by FINSEQ_1:def 4;

        then

        reconsider ntv1 as Element of (D() * ) by FINSEQ_1:def 11;

        reconsider tss = ts as Element of (( TS DT()) * ) by FINSEQ_1:def 11;

        

        thus (f1() . (nt -tree ts)) = H(nt,tss,ntv1) by A2, A6

        .= (f2() . (nt -tree ts)) by A4, A6, A10, A11, A12, FUNCT_1: 2;

      end;

      

       A15: for s be Symbol of DT() st s in ( Terminals DT()) holds P[( root-tree s)]

      proof

        let s be Symbol of DT();

        assume

         A16: s in ( Terminals DT());

        

        hence (f1() . ( root-tree s)) = G(s) by A1

        .= (f2() . ( root-tree s)) by A3, A16;

      end;

      for t be DecoratedTree of the carrier of DT() st t in ( TS DT()) holds P[t] from DTCONSTR:sch 7( A15, A5);

      then for x be object st x in ( TS DT()) holds (f1() . x) = (f2() . x);

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MSAFREE1:2

    

     Th2: for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds for o,b be object st [o, b] in ( REL X) holds o in [:the carrier' of S, {the carrier of S}:] & b in (( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))) * )

    proof

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

      let o,b be object;

      assume

       A1: [o, b] in ( REL X);

      then

      reconsider o9 = o as Element of ( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))) by ZFMISC_1: 87;

      reconsider b9 = b as Element of (( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))) * ) by A1, ZFMISC_1: 87;

      

       A2: [o9, b9] in ( REL X) by A1;

      hence o in [:the carrier' of S, {the carrier of S}:] by MSAFREE:def 7;

      thus thesis by A2;

    end;

    theorem :: MSAFREE1:3

    for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds for o be OperSymbol of S, b be FinSequence st [ [o, the carrier of S], b] in ( REL X) holds ( len b) = ( len ( the_arity_of o)) & for x be set st x in ( dom b) holds ((b . x) in [:the carrier' of S, {the carrier of S}:] implies for o1 be OperSymbol of S st [o1, the carrier of S] = (b . x) holds ( the_result_sort_of o1) = (( the_arity_of o) . x)) & ((b . x) in ( Union ( coprod X)) implies (b . x) in ( coprod ((( the_arity_of o) . x),X)))

    proof

      let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S, o be OperSymbol of S, b be FinSequence;

      assume

       A1: [ [o, the carrier of S], b] in ( REL X);

      then

      reconsider b9 = b as Element of (( [:the carrier' of S, {the carrier of S}:] \/ ( Union ( coprod X))) * ) by Th2;

      ( len b9) = ( len ( the_arity_of o)) by A1, MSAFREE: 5;

      hence ( len b) = ( len ( the_arity_of o));

      for x be set st x in ( dom b9) holds ((b9 . x) in [:the carrier' of S, {the carrier of S}:] implies for o1 be OperSymbol of S st [o1, the carrier of S] = (b9 . x) holds ( the_result_sort_of o1) = (( the_arity_of o) . x)) & ((b9 . x) in ( Union ( coprod X)) implies (b9 . x) in ( coprod ((( the_arity_of o) . x),X))) by A1, MSAFREE: 5;

      hence thesis;

    end;

    registration

      let I be non empty set, M be ManySortedSet of I;

      cluster ( rng M) -> non empty;

      coherence ;

    end

    registration

      let I be set;

      cluster empty-yielding -> disjoint_valued for ManySortedSet of I;

      coherence

      proof

        let M be ManySortedSet of I such that

         A1: M is empty-yielding;

        let x,y be object;

        assume x <> y;

        per cases ;

          suppose x in ( dom M) & y in ( dom M);

          (M . x) is empty by A1;

          hence thesis by XBOOLE_1: 65;

        end;

          suppose not (x in ( dom M) & y in ( dom M));

          then (M . x) = {} or (M . y) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

    end

    registration

      let I be set;

      cluster disjoint_valued for ManySortedSet of I;

      existence

      proof

        set M = the empty-yielding ManySortedSet of I;

        take M;

        thus thesis;

      end;

    end

    definition

      let I be non empty set;

      let X be disjoint_valued ManySortedSet of I;

      let D be non-empty ManySortedSet of I;

      let F be ManySortedFunction of X, D;

      :: MSAFREE1:def1

      func Flatten F -> Function of ( Union X), ( Union D) means

      : Def1: for i be Element of I, x be set st x in (X . i) holds (it . x) = ((F . i) . x);

      existence

      proof

        defpred P[ object, object] means for i be Element of I st $1 in (X . i) holds $2 = ((F . i) . $1);

        

         A1: for x be object st x in ( Union X) holds ex y be object st y in ( Union D) & P[x, y]

        proof

          let e be object;

          assume e in ( Union X);

          then

          consider i be object such that

           A2: i in ( dom X) and

           A3: e in (X . i) by CARD_5: 2;

          reconsider i as Element of I by A2, PARTFUN1:def 2;

          take u = ((F . i) . e);

          i in I;

          then

           A4: i in ( dom D) by PARTFUN1:def 2;

          ((F . i) . e) in (D . i) by A3, FUNCT_2: 5;

          hence u in ( Union D) by A4, CARD_5: 2;

          let i9 be Element of I;

          assume e in (X . i9);

          then (X . i9) meets (X . i) by A3, XBOOLE_0: 3;

          hence thesis by PROB_2:def 2;

        end;

        consider f be Function of ( Union X), ( Union D) such that

         A5: for e be object st e in ( Union X) holds P[e, (f . e)] from FUNCT_2:sch 1( A1);

        take f;

        let i be Element of I, x be set;

        assume

         A6: x in (X . i);

        i in I;

        then i in ( dom X) by PARTFUN1:def 2;

        then x in ( Union X) by A6, CARD_5: 2;

        hence thesis by A5, A6;

      end;

      correctness

      proof

        let F1,F2 be Function of ( Union X), ( Union D) such that

         A7: for i be Element of I, x be set st x in (X . i) holds (F1 . x) = ((F . i) . x) and

         A8: for i be Element of I, x be set st x in (X . i) holds (F2 . x) = ((F . i) . x);

        now

          let x be object;

          assume x in ( Union X);

          then

          consider i be object such that

           A9: i in ( dom X) and

           A10: x in (X . i) by CARD_5: 2;

          reconsider i as Element of I by A9, PARTFUN1:def 2;

          

          thus (F1 . x) = ((F . i) . x) by A7, A10

          .= (F2 . x) by A8, A10;

        end;

        hence F1 = F2 by FUNCT_2: 12;

      end;

    end

    theorem :: MSAFREE1:4

    

     Th4: for I be non empty set, X be disjoint_valued ManySortedSet of I, D be non-empty ManySortedSet of I holds for F1,F2 be ManySortedFunction of X, D st ( Flatten F1) = ( Flatten F2) holds F1 = F2

    proof

      let I be non empty set, X be disjoint_valued ManySortedSet of I, D be non-empty ManySortedSet of I;

      let F1,F2 be ManySortedFunction of X, D;

      assume

       A1: ( Flatten F1) = ( Flatten F2);

      now

        let i be object;

        assume

         A2: i in I;

        then

        reconsider Di = (D . i) as non empty set;

        reconsider f1 = (F1 . i), f2 = (F2 . i) as Function of (X . i), Di by A2, PBOOLE:def 15;

        now

          let x be object;

          assume

           A3: x in (X . i);

          

          hence (f1 . x) = (( Flatten F1) . x) by A2, Def1

          .= (f2 . x) by A1, A2, A3, Def1;

        end;

        hence (F1 . i) = (F2 . i) by FUNCT_2: 12;

      end;

      hence thesis;

    end;

    definition

      let S be non empty ManySortedSign;

      let A be MSAlgebra over S;

      :: MSAFREE1:def2

      attr A is disjoint_valued means

      : Def2: the Sorts of A is disjoint_valued;

    end

    definition

      let S be non empty ManySortedSign;

      :: MSAFREE1:def3

      func SingleAlg S -> strict MSAlgebra over S means

      : Def3: for i be set st i in the carrier of S holds (the Sorts of it . i) = {i};

      existence

      proof

        deffunc F( object) = {$1};

        consider f be ManySortedSet of the carrier of S such that

         A1: for i be object st i in the carrier of S holds (f . i) = F(i) from PBOOLE:sch 4;

        set Ch = the ManySortedFunction of ((f # ) * the Arity of S), (f * the ResultSort of S);

        take MSAlgebra (# f, Ch #);

        thus thesis by A1;

      end;

      uniqueness

      proof

        let A1,A2 be strict MSAlgebra over S such that

         A2: for i be set st i in the carrier of S holds (the Sorts of A1 . i) = {i} and

         A3: for i be set st i in the carrier of S holds (the Sorts of A2 . i) = {i};

        set B = the Sorts of A1;

        now

          let i be object;

          assume

           A4: i in the carrier of S;

          

          hence (the Sorts of A1 . i) = {i} by A2

          .= (the Sorts of A2 . i) by A3, A4;

        end;

        then

         A5: the Sorts of A1 = the Sorts of A2;

        

         A6: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

        now

          let i be object;

          set A = ((B * the ResultSort of S) . i);

          assume

           A7: i in the carrier' of S;

          

          then

           A8: A = (B . (the ResultSort of S . i)) by A6, FUNCT_1: 13

          .= {(the ResultSort of S . i)} by A2, A7, FUNCT_2: 5;

          then

          reconsider A as non empty set;

          reconsider f1 = (the Charact of A1 . i), f2 = (the Charact of A2 . i) as Function of (((B # ) * the Arity of S) . i), A by A5, A7, PBOOLE:def 15;

          now

            let x be object;

            assume

             A9: x in (((B # ) * the Arity of S) . i);

            then (f1 . x) in A by FUNCT_2: 5;

            then

             A10: (f1 . x) = (the ResultSort of S . i) by A8, TARSKI:def 1;

            (f2 . x) in A by A9, FUNCT_2: 5;

            hence (f1 . x) = (f2 . x) by A8, A10, TARSKI:def 1;

          end;

          hence (the Charact of A1 . i) = (the Charact of A2 . i) by FUNCT_2: 12;

        end;

        hence thesis by A5, PBOOLE: 3;

      end;

    end

    

     Lm1: for S be non empty ManySortedSign holds ( SingleAlg S) is non-empty disjoint_valued

    proof

      let S be non empty ManySortedSign;

      set F = the Sorts of ( SingleAlg S);

      hereby

        let x be object;

        assume x in the carrier of S;

        then (F . x) = {x} by Def3;

        hence (F . x) is non empty;

      end;

      let x,y be object such that

       A1: x <> y;

      per cases ;

        suppose

         A2: x in ( dom F) & y in ( dom F);

        ( dom F) = the carrier of S by PARTFUN1:def 2;

        then

         A3: (F . x) = {x} & (F . y) = {y} by A2, Def3;

        assume (F . x) meets (F . y);

        hence contradiction by A1, A3, ZFMISC_1: 11;

      end;

        suppose not (x in ( dom F) & y in ( dom F));

        then (F . x) = {} or (F . y) = {} by FUNCT_1:def 2;

        hence thesis by XBOOLE_1: 65;

      end;

    end;

    registration

      let S be non empty ManySortedSign;

      cluster non-empty disjoint_valued for MSAlgebra over S;

      existence

      proof

        ( SingleAlg S) is non-empty disjoint_valued by Lm1;

        hence thesis;

      end;

    end

    registration

      let S be non empty ManySortedSign;

      cluster ( SingleAlg S) -> non-empty disjoint_valued;

      coherence by Lm1;

    end

    registration

      let S be non empty ManySortedSign;

      let A be disjoint_valued MSAlgebra over S;

      cluster the Sorts of A -> disjoint_valued;

      coherence by Def2;

    end

    theorem :: MSAFREE1:5

    

     Th5: for S be non void non empty ManySortedSign, o be OperSymbol of S, A1 be non-empty disjoint_valued MSAlgebra over S, A2 be non-empty MSAlgebra over S, f be ManySortedFunction of A1, A2, a be Element of ( Args (o,A1)) holds (( Flatten f) * a) = (f # a)

    proof

      let S be non void non empty ManySortedSign, o be OperSymbol of S, A1 be non-empty disjoint_valued MSAlgebra over S, A2 be non-empty MSAlgebra over S, f be ManySortedFunction of A1, A2, a be Element of ( Args (o,A1));

      

       A1: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      set s = ( the_arity_of o);

      a in (((the Sorts of A1 # ) * the Arity of S) . o);

      then a in ((the Sorts of A1 # ) . (the Arity of S . o)) by A1, FUNCT_1: 13;

      then

       A2: a in ( product (the Sorts of A1 * s)) by FINSEQ_2:def 5;

      then ( rng a) c= ( Union (the Sorts of A1 * s)) by Th1;

      then ( union ( rng (the Sorts of A1 * s))) c= ( union ( rng the Sorts of A1)) & ( rng a) c= ( union ( rng (the Sorts of A1 * s))) by CARD_3:def 4, RELAT_1: 26, ZFMISC_1: 77;

      then ( rng a) c= ( union ( rng the Sorts of A1));

      then ( rng a) c= ( Union the Sorts of A1) by CARD_3:def 4;

      then ( rng a) c= ( dom ( Flatten f)) by FUNCT_2:def 1;

      then

       A3: ( dom (( Flatten f) * a)) = ( dom a) by RELAT_1: 27;

      

       A4: ( rng s) c= the carrier of S by FINSEQ_1:def 4;

      ( dom the Sorts of A1) = the carrier of S by PARTFUN1:def 2;

      then

       A5: ( dom (the Sorts of A1 * s)) = ( dom s) by A4, RELAT_1: 27;

      

       A6: ( dom a) = ( dom (the Sorts of A1 * s)) by A2, CARD_3: 9;

       A7:

      now

        let x be object;

        assume

         A8: x in ( dom (the Sorts of A2 * s));

        

         A9: ( dom (the Sorts of A2 * s)) c= ( dom s) by RELAT_1: 25;

        then

         A10: (the Sorts of A2 . (s . x)) = ((the Sorts of A2 * s) . x) by A8, FUNCT_1: 13;

        (s . x) in ( rng s) by A9, A8, FUNCT_1:def 3;

        then

        reconsider z = (s . x) as SortSymbol of S by A4;

        (the Sorts of A1 . (s . x)) = ((the Sorts of A1 * s) . x) by A9, A8, FUNCT_1: 13;

        then

         A11: (a . x) in (the Sorts of A1 . z) by A2, A5, A9, A8, CARD_3: 9;

        ((( Flatten f) * a) . x) = (( Flatten f) . (a . x)) by A6, A5, A9, A8, FUNCT_1: 13

        .= ((f . z) . (a . x)) by A11, Def1;

        hence ((( Flatten f) * a) . x) in ((the Sorts of A2 * s) . x) by A10, A11, FUNCT_2: 5;

      end;

      ( dom the Sorts of A2) = the carrier of S by PARTFUN1:def 2;

      then ( dom s) = ( dom (the Sorts of A2 * s)) by A4, RELAT_1: 27;

      then (( Flatten f) * a) in ( product (the Sorts of A2 * s)) by A3, A6, A5, A7, CARD_3: 9;

      then (( Flatten f) * a) in ((the Sorts of A2 # ) . (the Arity of S . o)) by FINSEQ_2:def 5;

      then

      reconsider x = (( Flatten f) * a) as Element of ( Args (o,A2)) by A1, FUNCT_1: 13;

      now

        let n be Nat;

        assume

         A12: n in ( dom a);

        then (( the_arity_of o) /. n) = (s . n) & (a . n) in ((the Sorts of A1 * s) . n) by A2, A6, A5, CARD_3: 9, PARTFUN1:def 6;

        then

         A13: (a . n) in (the Sorts of A1 . (( the_arity_of o) /. n)) by A6, A5, A12, FUNCT_1: 13;

        

        thus (x . n) = (( Flatten f) . (a . n)) by A12, FUNCT_1: 13

        .= ((f . (( the_arity_of o) /. n)) . (a . n)) by A13, Def1;

      end;

      hence thesis by MSUALG_3:def 6;

    end;

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeSort X) -> disjoint_valued;

      coherence

      proof

        let x,y be object;

        set F = ( FreeSort X);

        per cases ;

          suppose x in ( dom F) & y in ( dom F);

          then

          reconsider s1 = x, s2 = y as SortSymbol of S by PARTFUN1:def 2;

          assume x <> y;

          then (F . s1) misses (F . s2) by MSAFREE: 12;

          hence thesis;

        end;

          suppose

           A1: not (x in ( dom F) & y in ( dom F));

          assume x <> y;

          (F . x) = {} or (F . y) = {} by A1, FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 65;

        end;

      end;

    end

    scheme :: MSAFREE1:sch2

    FreeSortUniq { S() -> non void non empty ManySortedSign , X,D() -> non-empty ManySortedSet of the carrier of S() , G( set) -> Element of ( Union D()) , H( object, object, object) -> Element of ( Union D()) , f1,f2() -> ManySortedFunction of ( FreeSort X()), D() } :

f1() = f2()

      provided

       A1: for o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))) holds for x be Element of (( Union D()) * ) st x = (( Flatten f1()) * ts) holds ((f1() . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = H(o,ts,x)

       and

       A2: for s be SortSymbol of S(), y be set st y in ( FreeGen (s,X())) holds ((f1() . s) . y) = G(y)

       and

       A3: for o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))) holds for x be Element of (( Union D()) * ) st x = (( Flatten f2()) * ts) holds ((f2() . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = H(o,ts,x)

       and

       A4: for s be SortSymbol of S(), y be set st y in ( FreeGen (s,X())) holds ((f2() . s) . y) = G(y);

      reconsider D = ( Union D()) as non empty set;

      ( TS ( DTConMSA X())) = ( union ( rng ( FreeSort X()))) by MSAFREE: 11

      .= ( Union ( FreeSort X())) by CARD_3:def 4;

      then

      reconsider f1 = ( Flatten f1()), f2 = ( Flatten f2()) as Function of ( TS ( DTConMSA X())), D;

      deffunc O( Element of ( DTConMSA X()), Element of (( TS ( DTConMSA X())) * ), Element of (( Union D()) * )) = H(`1,$2,$3);

      consider H be Function of [:the carrier of ( DTConMSA X()), (( TS ( DTConMSA X())) * ), (( Union D()) * ):], ( Union D()) such that

       A5: for nt be Element of ( DTConMSA X()), ts be Element of (( TS ( DTConMSA X())) * ), x be Element of (( Union D()) * ) holds (H . (nt,ts,x)) = O(nt,ts,x) from MULTOP_1:sch 4;

      reconsider H as Function of [:the carrier of ( DTConMSA X()), (( TS ( DTConMSA X())) * ), (D * ):], D;

      deffunc Hf( Element of ( DTConMSA X()), Element of (( TS ( DTConMSA X())) * ), Element of (D * )) = (H . ($1,$2,$3));

      

       A6: ( DTConMSA X()) = DTConstrStr (# ( [:the carrier' of S(), {the carrier of S()}:] \/ ( Union ( coprod X()))), ( REL X()) #) by MSAFREE:def 8;

       A7:

      now

        let f be ManySortedFunction of ( FreeSort X()), D() such that

         A8: for o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))) holds for x be Element of (D * ) st x = (( Flatten f) * ts) holds ((f . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = H(o,ts,x);

        let nt be Element of ( DTConMSA X()), ts be Element of (( TS ( DTConMSA X())) * );

        assume

         A9: nt ==> ( roots ts);

        then [nt, ( roots ts)] in ( REL X()) by A6, LANG1:def 1;

        then

        consider o be OperSymbol of S(), x2 be Element of {the carrier of S()} such that

         A10: nt = [o, x2] by Th2, DOMAIN_1: 1;

        let x be Element of (D * );

        assume

         A11: x = (( Flatten f) * ts);

        

         A12: ( FreeMSA X()) = MSAlgebra (# ( FreeSort X()), ( FreeOper X()) #) by MSAFREE:def 14;

        reconsider tss = ts as FinSequence of ( TS ( DTConMSA X())) by FINSEQ_1:def 11;

        reconsider xx = x as Element of (( Union D()) * );

        

         A13: x2 = the carrier of S() by TARSKI:def 1;

        then

         A14: nt = ( Sym (o,X())) by A10, MSAFREE:def 9;

        then

         A15: tss in (((( FreeSort X()) # ) * the Arity of S()) . o) by A9, MSAFREE: 10;

        ((( FreeSort X()) * the ResultSort of S()) . o) = (( FreeSort X()) . ( the_result_sort_of o)) by FUNCT_2: 15;

        then

         A16: (( DenOp (o,X())) . ts) in (( FreeSort X()) . ( the_result_sort_of o)) by A15, FUNCT_2: 5;

        (( Flatten f) . ( [o, the carrier of S()] -tree ts)) = (( Flatten f) . (( DenOp (o,X())) . tss)) by A9, A10, A13, A14, MSAFREE:def 12

        .= ((f . ( the_result_sort_of o)) . (( DenOp (o,X())) . ts)) by A16, Def1

        .= ((f . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) by A12, MSAFREE:def 13

        .= H(o,ts,x) by A8, A12, A15, A11

        .= H(`1,ts,x) by A10;

        

        hence (( Flatten f) . (nt -tree ts)) = O(nt,ts,xx) by A10, A13

        .= (H . (nt,ts,x)) by A5;

      end;

      then

       A17: for nt be Symbol of ( DTConMSA X()), ts be Element of (( TS ( DTConMSA X())) * ) st nt ==> ( roots ts) holds for x be Element of (D * ) st x = (f1 * ts) holds (f1 . (nt -tree ts)) = Hf(nt,ts,x) by A1;

      deffunc F( Element of ( DTConMSA X())) = G(root-tree);

      

       A18: ( Terminals ( DTConMSA X())) = ( Union ( coprod X())) by MSAFREE: 6;

      consider G be Function of the carrier of ( DTConMSA X()), ( Union D()) such that

       A19: for t be Element of ( DTConMSA X()) holds (G . t) = F(t) from FUNCT_2:sch 4;

      reconsider G as Function of the carrier of ( DTConMSA X()), D;

      deffunc Gf( Element of ( DTConMSA X())) = (G . $1);

      

       A20: ( dom X()) = the carrier of S() by PARTFUN1:def 2;

       A21:

      now

        let f be ManySortedFunction of ( FreeSort X()), D() such that

         A22: for s be SortSymbol of S(), y be set st y in ( FreeGen (s,X())) holds ((f . s) . y) = G(y);

        let t be Element of ( DTConMSA X());

        assume

         A23: t in ( Terminals ( DTConMSA X()));

        then

        reconsider s = (t `2 ) as SortSymbol of S() by A18, A20, CARD_3: 22;

        (t `1 ) in (X() . (t `2 )) by A18, A23, CARD_3: 22;

        then

         A24: ( root-tree [(t `1 ), s]) in ( FreeGen (s,X())) by MSAFREE:def 15;

        

         A25: t = [(t `1 ), (t `2 )] by A18, A23, CARD_3: 22;

        

        hence (( Flatten f) . ( root-tree t)) = ((f . s) . ( root-tree [(t `1 ), s])) by A24, Def1

        .= G(root-tree) by A22, A25, A24

        .= (G . t) by A19;

      end;

      then

       A26: for t be Symbol of ( DTConMSA X()) st t in ( Terminals ( DTConMSA X())) holds (f2 . ( root-tree t)) = Gf(t) by A4;

      

       A27: for nt be Symbol of ( DTConMSA X()), ts be Element of (( TS ( DTConMSA X())) * ) st nt ==> ( roots ts) holds for x be Element of (D * ) st x = (f2 * ts) holds (f2 . (nt -tree ts)) = Hf(nt,ts,x) qua Element of D by A3, A7;

      

       A28: for t be Element of ( DTConMSA X()) st t in ( Terminals ( DTConMSA X())) holds (f1 . ( root-tree t)) = Gf(t) by A2, A21;

      f1 = f2 from DTConstrUniq( A28, A17, A26, A27);

      hence thesis by Th4;

    end;

    registration

      let S be non void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeMSA X) -> non-empty;

      coherence ;

    end

    registration

      let S be non void non empty ManySortedSign;

      let o be OperSymbol of S;

      let A be non-empty MSAlgebra over S;

      cluster ( Args (o,A)) -> non empty;

      coherence ;

      cluster ( Result (o,A)) -> non empty;

      coherence ;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S;

      cluster the Sorts of ( FreeMSA X) -> disjoint_valued;

      coherence

      proof

        ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

        hence thesis;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeMSA X) -> disjoint_valued;

      coherence ;

    end

    scheme :: MSAFREE1:sch3

    ExtFreeGen { S() -> non void non empty ManySortedSign , X() -> non-empty ManySortedSet of the carrier of S() , MSA() -> non-empty MSAlgebra over S() , P[ object, object, object], IT1,IT2() -> ManySortedFunction of ( FreeMSA X()), MSA() } :

IT1() = IT2()

      provided

       A1: IT1() is_homomorphism (( FreeMSA X()),MSA())

       and

       A2: for s be SortSymbol of S(), x,y be set st y in ( FreeGen (s,X())) holds ((IT1() . s) . y) = x iff P[s, x, y]

       and

       A3: IT2() is_homomorphism (( FreeMSA X()),MSA())

       and

       A4: for s be SortSymbol of S(), x,y be set st y in ( FreeGen (s,X())) holds ((IT2() . s) . y) = x iff P[s, x, y];

      defpred Z[ object, object] means for s be SortSymbol of S() st $1 in ( FreeGen (s,X())) holds P[s, $2, $1];

      

       A5: ( FreeMSA X()) = MSAlgebra (# ( FreeSort X()), ( FreeOper X()) #) by MSAFREE:def 14;

      then

      reconsider f1 = IT1(), f2 = IT2() as ManySortedFunction of ( FreeSort X()), the Sorts of MSA();

      

       A6: for x be object st x in ( Union ( FreeGen X())) holds ex y be object st y in ( Union the Sorts of MSA()) & Z[x, y]

      proof

        let e be object;

        

         A7: ( dom the Sorts of MSA()) = the carrier of S() by PARTFUN1:def 2;

        assume e in ( Union ( FreeGen X()));

        then

        consider s be object such that

         A8: s in ( dom ( FreeGen X())) and

         A9: e in (( FreeGen X()) . s) by CARD_5: 2;

        reconsider s as SortSymbol of S() by A8, PARTFUN1:def 2;

        

         A10: e in ( FreeGen (s,X())) by A9, MSAFREE:def 16;

        take u = ((IT1() . s) . e);

        (f1 . s) is Function of (( FreeSort X()) . s), (the Sorts of MSA() . s);

        then u in (the Sorts of MSA() . s) by A10, FUNCT_2: 5;

        hence u in ( Union the Sorts of MSA()) by A7, CARD_5: 2;

        let s9 be SortSymbol of S();

        assume

         A11: e in ( FreeGen (s9,X()));

        then ((( FreeSort X()) . s9) /\ (( FreeSort X()) . s)) <> {} by A10, XBOOLE_0:def 4;

        then (( FreeSort X()) . s9) meets (( FreeSort X()) . s) by XBOOLE_0:def 7;

        then s = s9 by MSAFREE: 12;

        hence thesis by A2, A11;

      end;

      consider G be Function of ( Union ( FreeGen X())), ( Union the Sorts of MSA()) such that

       A12: for e be object st e in ( Union ( FreeGen X())) holds Z[e, (G . e)] from FUNCT_2:sch 1( A6);

      deffunc Gf( set) = (G /. $1);

      defpred P[ object, object] means for o be OperSymbol of S(), a be Element of ( Args (o,MSA())) st $1 = [o, a] holds $2 = (( Den (o,MSA())) . a);

      consider R be set such that

       A13: R = the set of all [o, a] where o be Element of the carrier' of S(), a be Element of ( Args (o,MSA()));

      

       A14: for s be SortSymbol of S(), y be set st y in ( FreeGen (s,X())) holds ((f1 . s) . y) = Gf(y)

      proof

        let s be SortSymbol of S(), y be set;

        

         A15: ( dom ( FreeGen X())) = the carrier of S() by PARTFUN1:def 2;

        assume

         A16: y in ( FreeGen (s,X()));

        then y in (( FreeGen X()) . s) by MSAFREE:def 16;

        then

         A17: y in ( Union ( FreeGen X())) by A15, CARD_5: 2;

        then P[s, (G . y), y] by A12, A16;

        

        hence ((f1 . s) . y) = (G . y) by A2, A16

        .= (G /. y) by A17, FUNCT_2:def 13;

      end;

      

       A18: for x be object st x in R holds ex y be object st y in ( Union the Sorts of MSA()) & P[x, y]

      proof

        let e be object;

        assume e in R;

        then

        consider o be OperSymbol of S(), a be Element of ( Args (o,MSA())) such that

         A19: e = [o, a] by A13;

        reconsider u = (( Den (o,MSA())) . a) as set;

        take u;

        u in ( union ( rng the Sorts of MSA())) by TARSKI:def 4;

        hence u in ( Union the Sorts of MSA()) by CARD_3:def 4;

        let o9 be OperSymbol of S(), x9 be Element of ( Args (o9,MSA()));

        assume

         A20: e = [o9, x9];

        then o = o9 by A19, XTUPLE_0: 1;

        hence thesis by A19, A20, XTUPLE_0: 1;

      end;

      consider H be Function of R, ( Union the Sorts of MSA()) such that

       A21: for e be object st e in R holds P[e, (H . e)] from FUNCT_2:sch 1( A18);

      

       A22: for s be SortSymbol of S(), y be set st y in ( FreeGen (s,X())) holds ((f2 . s) . y) = Gf(y)

      proof

        let s be SortSymbol of S(), y be set;

        

         A23: ( dom ( FreeGen X())) = the carrier of S() by PARTFUN1:def 2;

        assume

         A24: y in ( FreeGen (s,X()));

        then y in (( FreeGen X()) . s) by MSAFREE:def 16;

        then

         A25: y in ( Union ( FreeGen X())) by A23, CARD_5: 2;

        then P[s, (G . y), y] by A12, A24;

        

        hence ((f2 . s) . y) = (G . y) by A4, A24

        .= (G /. y) by A25, FUNCT_2:def 13;

      end;

      deffunc Hf( set, set, set) = (H /. [$1, $3]);

      

       A26: for o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))) holds for x be Element of (( Union the Sorts of MSA()) * ) st x = (( Flatten f2) * ts) holds ((f2 . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = Hf(o,ts,x)

      proof

        let o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))), x be Element of (( Union the Sorts of MSA()) * );

        assume

         A27: x = (( Flatten f2) * ts);

        

         A28: (( Flatten f2) * ts) = (IT2() # ts) by A5, Th5;

        then

        reconsider a = x as Element of ( Args (o,MSA())) by A27;

        

         A29: [o, a] in R by A13;

        

        thus ((f2 . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = (( Den (o,MSA())) . a) by A3, A28, A27, MSUALG_3:def 7

        .= (H . [o, x]) by A21, A29

        .= (H /. [o, x]) by A29, FUNCT_2:def 13;

      end;

      

       A30: for o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))) holds for x be Element of (( Union the Sorts of MSA()) * ) st x = (( Flatten f1) * ts) holds ((f1 . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = Hf(o,ts,x)

      proof

        let o be OperSymbol of S(), ts be Element of ( Args (o,( FreeMSA X()))), x be Element of (( Union the Sorts of MSA()) * );

        assume

         A31: x = (( Flatten f1) * ts);

        

         A32: (( Flatten f1) * ts) = (IT1() # ts) by A5, Th5;

        then

        reconsider a = x as Element of ( Args (o,MSA())) by A31;

        

         A33: [o, a] in R by A13;

        

        thus ((f1 . ( the_result_sort_of o)) . (( Den (o,( FreeMSA X()))) . ts)) = (( Den (o,MSA())) . a) by A1, A32, A31, MSUALG_3:def 7

        .= (H . [o, x]) by A21, A33

        .= (H /. [o, x]) by A33, FUNCT_2:def 13;

      end;

      f1 = f2 from FreeSortUniq( A30, A14, A26, A22);

      hence thesis;

    end;