msalimit.miz



    begin

    reserve P for non empty Poset,

i,j,k for Element of P;

    reserve S for non void non empty ManySortedSign;

    registration

      let I be non empty set, S;

      let AF be MSAlgebra-Family of I, S;

      let i be Element of I;

      let o be OperSymbol of S;

      cluster ((( OPER AF) . i) . o) -> Function-like Relation-like;

      coherence

      proof

        ex U0 be MSAlgebra over S st U0 = (AF . i) & (( OPER AF) . i) = the Charact of U0 by PRALG_2:def 11;

        hence thesis;

      end;

    end

    registration

      let I be non empty set, S;

      let AF be MSAlgebra-Family of I, S;

      let s be SortSymbol of S;

      cluster (( SORTS AF) . s) -> functional;

      coherence

      proof

        (( SORTS AF) . s) = ( product ( Carrier (AF,s))) by PRALG_2:def 10;

        hence thesis;

      end;

    end

    definition

      let P, S;

      :: MSALIMIT:def1

      mode OrderedAlgFam of P,S -> MSAlgebra-Family of the carrier of P, S means

      : Def1: ex F be ManySortedFunction of the InternalRel of P st for i, j, k st i >= j & j >= k holds ex f1 be ManySortedFunction of (it . i), (it . j), f2 be ManySortedFunction of (it . j), (it . k) st f1 = (F . (j,i)) & f2 = (F . (k,j)) & (F . (k,i)) = (f2 ** f1) & f1 is_homomorphism ((it . i),(it . j));

      existence

      proof

        reconsider T1 = the InternalRel of P as Relation of the carrier of P;

        set A = the non-empty MSAlgebra over S;

        reconsider Z = (the carrier of P --> A) as ManySortedSet of the carrier of P;

        for i be object st i in the carrier of P holds (Z . i) is non-empty MSAlgebra over S by FUNCOP_1: 7;

        then

        reconsider Z as MSAlgebra-Family of the carrier of P, S by PRALG_2:def 5;

        take Z;

        set G = (the InternalRel of P --> ( id the Sorts of A));

        reconsider G as ManySortedFunction of the InternalRel of P;

        take G;

        let i, j, k;

        consider F2 be ManySortedFunction of (Z . j), (Z . k) such that

         A2: F2 = ( id the Sorts of A);

        assume i >= j & j >= k;

        then

         A3: [j, i] in the InternalRel of P & [k, j] in the InternalRel of P by ORDERS_2:def 5;

        ( field T1) = the carrier of P by ORDERS_1: 12;

        then T1 is_transitive_in the carrier of P by RELAT_2:def 16;

        then

         A4: [k, i] in T1 by A3, RELAT_2:def 8;

        consider F1 be ManySortedFunction of (Z . i), (Z . j) such that

         A6: F1 = ( id the Sorts of A);

        take F1;

        take F2;

        (F2 ** F1) = ( id the Sorts of A) by A6, A2, MSUALG_3: 3;

        hence thesis by A3, A6, A2, A4, FUNCOP_1: 7, MSUALG_3: 9;

      end;

    end

    reserve OAF for OrderedAlgFam of P, S;

    definition

      let P, S, OAF;

      :: MSALIMIT:def2

      mode Binding of OAF -> ManySortedFunction of the InternalRel of P means

      : Def2: for i, j, k st i >= j & j >= k holds ex f1 be ManySortedFunction of (OAF . i), (OAF . j), f2 be ManySortedFunction of (OAF . j), (OAF . k) st f1 = (it . (j,i)) & f2 = (it . (k,j)) & (it . (k,i)) = (f2 ** f1) & f1 is_homomorphism ((OAF . i),(OAF . j));

      existence by Def1;

    end

    definition

      let P, S, OAF;

      let B be Binding of OAF, i, j;

      assume

       A1: i >= j;

      :: MSALIMIT:def3

      func bind (B,i,j) -> ManySortedFunction of (OAF . i), (OAF . j) equals

      : Def3: (B . (j,i));

      coherence

      proof

        j >= j by ORDERS_2: 1;

        then ex f1 be ManySortedFunction of (OAF . i), (OAF . j), f2 be ManySortedFunction of (OAF . j), (OAF . j) st f1 = (B . (j,i)) & f2 = (B . (j,j)) & (B . (j,i)) = (f2 ** f1) & f1 is_homomorphism ((OAF . i),(OAF . j)) by A1, Def2;

        hence thesis;

      end;

    end

    reserve B for Binding of OAF;

    theorem :: MSALIMIT:1

    

     Th1: i >= j & j >= k implies (( bind (B,j,k)) ** ( bind (B,i,j))) = ( bind (B,i,k))

    proof

      assume

       A1: i >= j & j >= k;

      then

       A2: ex f1 be ManySortedFunction of (OAF . i), (OAF . j), f2 be ManySortedFunction of (OAF . j), (OAF . k) st f1 = (B . (j,i)) & f2 = (B . (k,j)) & (B . (k,i)) = (f2 ** f1) & f1 is_homomorphism ((OAF . i),(OAF . j)) by Def2;

      ( bind (B,j,k)) = (B . (k,j)) & ( bind (B,i,j)) = (B . (j,i)) by A1, Def3;

      hence thesis by A1, A2, Def3, ORDERS_2: 3;

    end;

    definition

      let P, S, OAF;

      let IT be Binding of OAF;

      :: MSALIMIT:def4

      attr IT is normalized means

      : Def4: for i holds (IT . (i,i)) = ( id the Sorts of (OAF . i));

    end

    theorem :: MSALIMIT:2

    

     Th2: for P, S, OAF, B, i, j st i >= j holds for f be ManySortedFunction of (OAF . i), (OAF . j) st f = ( bind (B,i,j)) holds f is_homomorphism ((OAF . i),(OAF . j))

    proof

      let P, S, OAF, B, i, j;

      assume

       A1: i >= j;

      let f be ManySortedFunction of (OAF . i), (OAF . j);

      assume

       A2: f = ( bind (B,i,j));

      j >= j by ORDERS_2: 1;

      then ex f1 be ManySortedFunction of (OAF . i), (OAF . j), f2 be ManySortedFunction of (OAF . j), (OAF . j) st f1 = (B . (j,i)) & f2 = (B . (j,j)) & (B . (j,i)) = (f2 ** f1) & f1 is_homomorphism ((OAF . i),(OAF . j)) by A1, Def2;

      hence thesis by A1, A2, Def3;

    end;

    definition

      let P, S, OAF, B;

      :: MSALIMIT:def5

      func Normalized B -> Binding of OAF means

      : Def5: for i, j st i >= j holds (it . (j,i)) = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i)))));

      existence

      proof

        defpred P[ object, object] means ex i, j st $1 = [j, i] & $2 = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i)))));

         A1:

        now

          let ij be object;

          assume

           A2: ij in the InternalRel of P;

          then

          reconsider i2 = (ij `1 ), i1 = (ij `2 ) as Element of P by MCART_1: 10;

          reconsider i1, i2 as Element of P;

          deffunc Z( object) = ( IFEQ (i2,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,i2)) ** ( id the Sorts of (OAF . i1)))));

          consider A be ManySortedSet of the InternalRel of P such that

           A3: for ij be object st ij in the InternalRel of P holds (A . ij) = Z(ij) from PBOOLE:sch 4;

          take x = (A . ij);

          take i1, i2;

          thus ij = [i2, i1] & x = ( IFEQ (i2,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,i2)) ** ( id the Sorts of (OAF . i1))))) by A2, A3, MCART_1: 21;

        end;

        

         A4: for z be object st z in the InternalRel of P holds ex y be object st P[z, y]

        proof

          let z be object;

          assume z in the InternalRel of P;

          then ex y be set st P[z, y] by A1;

          hence thesis;

        end;

        consider A be ManySortedSet of the InternalRel of P such that

         A5: for ij be object st ij in the InternalRel of P holds P[ij, (A . ij)] from PBOOLE:sch 3( A4);

        for z be object st z in ( dom A) holds (A . z) is Function

        proof

          let z be object;

          assume z in ( dom A);

          then z in the InternalRel of P;

          then

          consider i1,i2 be Element of P such that z = [i2, i1] and

           A6: (A . z) = ( IFEQ (i2,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,i2)) ** ( id the Sorts of (OAF . i1))))) by A5;

          per cases ;

            suppose i1 = i2;

            hence thesis by A6, FUNCOP_1:def 8;

          end;

            suppose i1 <> i2;

            hence thesis by A6, FUNCOP_1:def 8;

          end;

        end;

        then

        reconsider A as ManySortedFunction of the InternalRel of P by FUNCOP_1:def 6;

        now

          let i, j, k;

          assume that

           A7: i >= j and

           A8: j >= k;

          consider kl be set such that

           A9: kl = [j, i];

          kl in the InternalRel of P by A7, A9, ORDERS_2:def 5;

          then

          consider i1,j1 be Element of P such that

           A10: [j1, i1] = kl and

           A11: (A . kl) = ( IFEQ (j1,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,j1)) ** ( id the Sorts of (OAF . i1))))) by A5;

          

           A12: i1 = i & j1 = j by A9, A10, XTUPLE_0: 1;

          (A . (j,i)) is ManySortedFunction of (OAF . i), (OAF . j)

          proof

            per cases ;

              suppose i = j;

              hence thesis by A10, A11, A12, FUNCOP_1:def 8;

            end;

              suppose i <> j;

              hence thesis by A10, A11, A12, FUNCOP_1:def 8;

            end;

          end;

          then

          reconsider f1 = (A . (j,i)) as ManySortedFunction of (OAF . i), (OAF . j);

          consider lm be set such that

           A13: lm = [k, j];

          lm in the InternalRel of P by A8, A13, ORDERS_2:def 5;

          then

          consider i2,j2 be Element of P such that

           A14: [j2, i2] = lm and

           A15: (A . lm) = ( IFEQ (j2,i2,( id the Sorts of (OAF . i2)),(( bind (B,i2,j2)) ** ( id the Sorts of (OAF . i2))))) by A5;

          

           A16: j2 = k & i2 = j by A13, A14, XTUPLE_0: 1;

          (A . (k,j)) is ManySortedFunction of (OAF . j), (OAF . k)

          proof

            per cases ;

              suppose j = k;

              hence thesis by A14, A15, A16, FUNCOP_1:def 8;

            end;

              suppose j <> k;

              hence thesis by A14, A15, A16, FUNCOP_1:def 8;

            end;

          end;

          then

          reconsider f2 = (A . (k,j)) as ManySortedFunction of (OAF . j), (OAF . k);

          

           A17: for i, j st i >= j & i <> j holds (A . (j,i)) = ( bind (B,i,j))

          proof

            let i, j;

            assume that

             A18: i >= j and

             A19: i <> j;

            consider lm be set such that

             A20: lm = [j, i];

            lm in the InternalRel of P by A18, A20, ORDERS_2:def 5;

            then

            consider i2,j2 be Element of P such that

             A21: [j2, i2] = lm and

             A22: (A . lm) = ( IFEQ (j2,i2,( id the Sorts of (OAF . i2)),(( bind (B,i2,j2)) ** ( id the Sorts of (OAF . i2))))) by A5;

            i2 = i & j2 = j by A20, A21, XTUPLE_0: 1;

            then (A . (j,i)) = (( bind (B,i,j)) ** ( id the Sorts of (OAF . i))) by A19, A21, A22, FUNCOP_1:def 8;

            hence thesis by MSUALG_3: 3;

          end;

          

           A23: (A . (k,i)) = (f2 ** f1)

          proof

            per cases ;

              suppose

               A24: i = j & j = k;

              then f2 = ( id the Sorts of (OAF . j)) by A14, A15, A16, FUNCOP_1:def 8;

              hence thesis by A24, MSUALG_3: 3;

            end;

              suppose

               A25: i = j & j <> k;

              then f1 = ( id the Sorts of (OAF . i)) by A10, A11, A12, FUNCOP_1:def 8;

              hence thesis by A25, MSUALG_3: 3;

            end;

              suppose

               A26: i <> j & j = k;

              then f2 = ( id the Sorts of (OAF . j)) by A14, A15, A16, FUNCOP_1:def 8;

              hence thesis by A26, MSUALG_3: 4;

            end;

              suppose

               A27: i <> j & j <> k;

              then i > j & j > k by A7, A8, ORDERS_2:def 6;

              then

               A28: i <> k by ORDERS_2: 5;

              f2 = (( bind (B,j,k)) ** ( id the Sorts of (OAF . j))) by A14, A15, A16, A27, FUNCOP_1:def 8;

              then

               A29: f2 = ( bind (B,j,k)) by MSUALG_3: 3;

              f1 = (( bind (B,i,j)) ** ( id the Sorts of (OAF . i))) by A10, A11, A12, A27, FUNCOP_1:def 8;

              then f1 = ( bind (B,i,j)) by MSUALG_3: 3;

              then (f2 ** f1) = ( bind (B,i,k)) by A7, A8, A29, Th1;

              hence thesis by A7, A8, A17, A28, ORDERS_2: 3;

            end;

          end;

          

           A30: for i, j st i = j holds (A . (j,i)) = ( id the Sorts of (OAF . i))

          proof

            let i, j;

            consider lm be set such that

             A31: lm = [j, i];

            assume

             A32: i = j;

            then i >= j by ORDERS_2: 1;

            then lm in the InternalRel of P by A31, ORDERS_2:def 5;

            then

            consider i2,j2 be Element of P such that

             A33: [j2, i2] = lm and

             A34: (A . lm) = ( IFEQ (j2,i2,( id the Sorts of (OAF . i2)),(( bind (B,i2,j2)) ** ( id the Sorts of (OAF . i2))))) by A5;

            i2 = i & j2 = j by A31, A33, XTUPLE_0: 1;

            hence thesis by A32, A33, A34, FUNCOP_1:def 8;

          end;

          f1 is_homomorphism ((OAF . i),(OAF . j))

          proof

            per cases ;

              suppose

               A35: i = j;

              then (A . (i,j)) = ( id the Sorts of (OAF . i)) by A30;

              hence thesis by A35, MSUALG_3: 9;

            end;

              suppose i <> j;

              then (A . (j,i)) = ( bind (B,i,j)) by A7, A17;

              hence thesis by A7, Th2;

            end;

          end;

          hence ex f1 be ManySortedFunction of (OAF . i), (OAF . j), f2 be ManySortedFunction of (OAF . j), (OAF . k) st f1 = (A . (j,i)) & f2 = (A . (k,j)) & (A . (k,i)) = (f2 ** f1) & f1 is_homomorphism ((OAF . i),(OAF . j)) by A23;

        end;

        then

        reconsider A as Binding of OAF by Def2;

        take A;

        let i, j;

        consider kl be set such that

         A36: kl = [j, i];

        assume i >= j;

        then kl in the InternalRel of P by A36, ORDERS_2:def 5;

        then

        consider i1,j1 be Element of P such that

         A37: [j1, i1] = kl and

         A38: (A . kl) = ( IFEQ (j1,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,j1)) ** ( id the Sorts of (OAF . i1))))) by A5;

        i1 = i & j1 = j by A36, A37, XTUPLE_0: 1;

        hence thesis by A37, A38;

      end;

      uniqueness

      proof

        let N1,N2 be Binding of OAF such that

         A39: for i, j st i >= j holds (N1 . (j,i)) = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i))))) and

         A40: for i, j st i >= j holds (N2 . (j,i)) = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i)))));

        now

          let ij be object;

          assume

           A41: ij in the InternalRel of P;

          then

          reconsider i2 = (ij `1 ), i1 = (ij `2 ) as Element of P by MCART_1: 10;

          reconsider i1, i2 as Element of P;

          

           A42: (N2 . ij) = (N2 . (i2,i1)) by A41, MCART_1: 21;

          ij = [(ij `1 ), (ij `2 )] by A41, MCART_1: 21;

          then

           A43: i2 <= i1 by A41, ORDERS_2:def 5;

          (N1 . ij) = (N1 . (i2,i1)) by A41, MCART_1: 21;

          then (N1 . ij) = ( IFEQ (i2,i1,( id the Sorts of (OAF . i1)),(( bind (B,i1,i2)) ** ( id the Sorts of (OAF . i1))))) by A39, A43;

          hence (N1 . ij) = (N2 . ij) by A40, A43, A42;

        end;

        hence N1 = N2 by PBOOLE: 3;

      end;

    end

    theorem :: MSALIMIT:3

    

     Th3: for i, j st i >= j & i <> j holds (B . (j,i)) = (( Normalized B) . (j,i))

    proof

      let i, j;

      assume that

       A1: i >= j and

       A2: i <> j;

      (( Normalized B) . (j,i)) = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i))))) & ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (B,i,j)) ** ( id the Sorts of (OAF . i))))) = (( bind (B,i,j)) ** ( id the Sorts of (OAF . i))) by A1, A2, Def5, FUNCOP_1:def 8;

      then (( Normalized B) . (j,i)) = ( bind (B,i,j)) by MSUALG_3: 3;

      hence thesis by A1, Def3;

    end;

    registration

      let P, S, OAF, B;

      cluster ( Normalized B) -> normalized;

      coherence

      proof

        let i be Element of P;

        i >= i by ORDERS_2: 1;

        then (( Normalized B) . (i,i)) = ( IFEQ (i,i,( id the Sorts of (OAF . i)),(( bind (B,i,i)) ** ( id the Sorts of (OAF . i))))) by Def5;

        hence thesis by FUNCOP_1:def 8;

      end;

    end

    registration

      let P, S, OAF;

      cluster normalized for Binding of OAF;

      existence

      proof

        set B = the Binding of OAF;

        take ( Normalized B);

        thus thesis;

      end;

    end

    theorem :: MSALIMIT:4

    for NB be normalized Binding of OAF holds for i, j st i >= j holds (( Normalized NB) . (j,i)) = (NB . (j,i))

    proof

      let NB be normalized Binding of OAF;

      let i, j;

      assume

       A1: i >= j;

      per cases ;

        suppose i <> j;

        hence thesis by A1, Th3;

      end;

        suppose

         A2: i = j;

        (( Normalized NB) . (j,i)) = ( IFEQ (j,i,( id the Sorts of (OAF . i)),(( bind (NB,i,j)) ** ( id the Sorts of (OAF . i))))) by A1, Def5;

        then (( Normalized NB) . (j,i)) = ( id the Sorts of (OAF . i)) by A2, FUNCOP_1:def 8;

        hence thesis by A2, Def4;

      end;

    end;

    definition

      let P, S, OAF;

      let B be Binding of OAF;

      :: MSALIMIT:def6

      func InvLim B -> strict MSSubAlgebra of ( product OAF) means

      : Def6: for s be SortSymbol of S holds for f be Element of (( SORTS OAF) . s) holds f in (the Sorts of it . s) iff for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j);

      existence

      proof

        reconsider L = ( product OAF) as non-empty MSAlgebra over S;

        deffunc F( SortSymbol of S) = { f where f be Element of ( product ( Carrier (OAF,$1))) : for i, j st i >= j holds ((( bind (B,i,j)) . $1) . (f . i)) = (f . j) };

        consider C be ManySortedSet of the carrier of S such that

         A1: for s be SortSymbol of S holds (C . s) = F(s) from PBOOLE:sch 5;

        for i be object st i in the carrier of S holds (C . i) c= (( SORTS OAF) . i)

        proof

          let i be object;

          assume i in the carrier of S;

          then

          reconsider s = i as SortSymbol of S;

          defpred P[ Element of ( product ( Carrier (OAF,s)))] means for i, j st i >= j holds ((( bind (B,i,j)) . s) . ($1 . i)) = ($1 . j);

          

           A2: { f where f be Element of ( product ( Carrier (OAF,s))) : P[f] } c= ( product ( Carrier (OAF,s))) from FRAENKEL:sch 10;

          (( SORTS OAF) . s) = ( product ( Carrier (OAF,s))) by PRALG_2:def 10;

          hence thesis by A1, A2;

        end;

        then C c= ( SORTS OAF) by PBOOLE:def 2;

        then

        reconsider C as ManySortedSubset of ( SORTS OAF) by PBOOLE:def 18;

        reconsider C as MSSubset of ( product OAF) by PRALG_2: 12;

        for o be OperSymbol of S holds C is_closed_on o

        proof

          let o be OperSymbol of S;

          ( rng (( Den (o,( product OAF))) | (((C # ) * the Arity of S) . o))) c= ((C * the ResultSort of S) . o)

          proof

            reconsider MS = C as ManySortedSet of the carrier of S;

            reconsider K = (( Den (o,( product OAF))) | (((C # ) * the Arity of S) . o)) as Function;

            let x be object;

            

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

            assume

             A4: x in ( rng (( Den (o,( product OAF))) | (((C # ) * the Arity of S) . o)));

            then

            consider y be object such that

             A5: y in ( dom K) and

             A6: x = (K . y) by FUNCT_1:def 3;

            

             A7: ( dom K) = (( dom ( Den (o,( product OAF)))) /\ (((C # ) * the Arity of S) . o)) by RELAT_1: 61;

            then y in (((C # ) * the Arity of S) . o) by A5, XBOOLE_0:def 4;

            then y in ((C # ) . (the Arity of S . o)) by A3, FUNCT_1: 13;

            then y in ((C # ) . ( the_arity_of o)) by MSUALG_1:def 1;

            then

             A8: y in ( product (MS * ( the_arity_of o))) by FINSEQ_2:def 5;

            x in ( Result (o,( product OAF))) by A4;

            then ( dom the ResultSort of S) = the carrier' of S & x in ((the Sorts of ( product OAF) * the ResultSort of S) . o) by FUNCT_2:def 1, MSUALG_1:def 5;

            then x in (the Sorts of ( product OAF) . (the ResultSort of S . o)) by FUNCT_1: 13;

            then

             A9: x in (( SORTS OAF) . (the ResultSort of S . o)) by PRALG_2: 12;

            then

            reconsider x1 = x as Function;

            x in (( SORTS OAF) . ( the_result_sort_of o)) by A9, MSUALG_1:def 2;

            then

             A10: x is Element of ( product ( Carrier (OAF,( the_result_sort_of o)))) by PRALG_2:def 10;

            

             A11: y in ( dom ( Den (o,( product OAF)))) by A5, A7, XBOOLE_0:def 4;

            now

              let s be SortSymbol of S;

              for i, j st i >= j holds ((( bind (B,i,j)) . ( the_result_sort_of o)) . (x1 . i)) = (x1 . j)

              proof

                reconsider OPE = (( OPS OAF) . o) as Function;

                

                 A12: ( Den (o,( product OAF))) = (the Charact of ( product OAF) . o) by MSUALG_1:def 6

                .= (( OPS OAF) . o) by PRALG_2: 12;

                reconsider y as Function by A8;

                let i, j;

                assume

                 A13: i >= j;

                reconsider Co = ( commute y) as Function;

                set y1 = (( commute y) . i);

                

                 A14: ( dom y) = ( dom (MS * ( the_arity_of o))) by A8, CARD_3: 9;

                

                 A15: ( rng ( the_arity_of o)) c= ( dom MS)

                proof

                  let i be object;

                  assume i in ( rng ( the_arity_of o));

                  then i in the carrier of S;

                  hence thesis by PARTFUN1:def 2;

                end;

                then

                 A16: ( dom y) = ( dom ( the_arity_of o)) by A14, RELAT_1: 27;

                then

                 A17: ( dom y) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

                ( rng y) c= ( Funcs (the carrier of P, |.OAF.|))

                proof

                  let z be object;

                  assume z in ( rng y);

                  then

                  consider n be object such that

                   A18: n in ( dom y) and

                   A19: z = (y . n) by FUNCT_1:def 3;

                  

                   A20: n in ( dom (MS * ( the_arity_of o))) by A8, A18, CARD_3: 9;

                  then n in ( dom ( the_arity_of o)) by A15, RELAT_1: 27;

                  then (( the_arity_of o) . n) = (( the_arity_of o) /. n) by PARTFUN1:def 6;

                  then

                  reconsider Pa = (( the_arity_of o) . n) as SortSymbol of S;

                  z in ((MS * ( the_arity_of o)) . n) by A8, A19, A20, CARD_3: 9;

                  then z in (MS . (( the_arity_of o) . n)) by A20, FUNCT_1: 12;

                  then z in { f where f be Element of ( product ( Carrier (OAF,Pa))) : for i, j st i >= j holds ((( bind (B,i,j)) . Pa) . (f . i)) = (f . j) } by A1;

                  then

                   A21: ex z9 be Element of ( product ( Carrier (OAF,Pa))) st z9 = z & for i, j st i >= j holds ((( bind (B,i,j)) . Pa) . (z9 . i)) = (z9 . j);

                  then

                  reconsider z as Function;

                  

                   A22: ( dom z) = ( dom ( Carrier (OAF,Pa))) by A21, CARD_3: 9

                  .= the carrier of P by PARTFUN1:def 2;

                  ( rng z) c= |.OAF.|

                  proof

                    let p be object;

                    assume p in ( rng z);

                    then

                    consider r be object such that

                     A23: r in ( dom z) and

                     A24: (z . r) = p by FUNCT_1:def 3;

                    reconsider r9 = r as Element of P by A22, A23;

                    reconsider r9 as Element of P;

                    r9 in the carrier of P;

                    then

                     A25: ex U0 be MSAlgebra over S st U0 = (OAF . r) & (( Carrier (OAF,Pa)) . r) = (the Sorts of U0 . Pa) by PRALG_2:def 9;

                     |.(OAF . r9).| in the set of all |.(OAF . k).| where k be Element of P;

                    then |.(OAF . r9).| c= ( union the set of all |.(OAF . k).| where k be Element of P) by ZFMISC_1: 74;

                    then

                     A26: |.(OAF . r9).| c= |.OAF.| by PRALG_2:def 7;

                    ( dom the Sorts of (OAF . r9)) = the carrier of S by PARTFUN1:def 2;

                    then

                     A27: (the Sorts of (OAF . r9) . Pa) in ( rng the Sorts of (OAF . r9)) by FUNCT_1:def 3;

                    ( dom z) = ( dom ( Carrier (OAF,Pa))) by A21, CARD_3: 9;

                    then p in (( Carrier (OAF,Pa)) . r) by A21, A23, A24, CARD_3: 9;

                    then p in ( union ( rng the Sorts of (OAF . r9))) by A25, A27, TARSKI:def 4;

                    then p in |.(OAF . r9).| by PRALG_2:def 6;

                    hence thesis by A26;

                  end;

                  hence thesis by A22, FUNCT_2:def 2;

                end;

                then

                 A28: y in ( Funcs (( Seg ( len ( the_arity_of o))),( Funcs (the carrier of P, |.OAF.|)))) by A17, FUNCT_2:def 2;

                per cases ;

                  suppose

                   A29: ( the_arity_of o) <> {} ;

                  

                   A30: for t be object st t in ( dom ( doms (OAF ?. o))) holds (Co . t) in (( doms (OAF ?. o)) . t)

                  proof

                    let t be object;

                    assume t in ( dom ( doms (OAF ?. o)));

                    then

                    reconsider t as Element of P by PRALG_2: 11;

                    reconsider yt = (Co . t) as Function;

                    ( dom ( the_arity_of o)) <> {} by A29;

                    then

                     WW: ( Seg ( len ( the_arity_of o))) <> {} by FINSEQ_1:def 3;

                    then Co in ( Funcs (the carrier of P,( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)))) by A28, FUNCT_6: 55;

                    then

                     A31: ex ss be Function st ss = Co & ( dom ss) = the carrier of P & ( rng ss) c= ( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)) by FUNCT_2:def 2;

                    

                     A32: (Co . t) in ( product (the Sorts of (OAF . t) * ( the_arity_of o)))

                    proof

                      

                       A33: ( dom (the Sorts of (OAF . t) * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3

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

                      

                       A34: ( dom y) = ( Seg ( len ( the_arity_of o))) by A16, FINSEQ_1:def 3;

                      

                       A35: for w be object st w in ( dom (the Sorts of (OAF . t) * ( the_arity_of o))) holds (yt . w) in ((the Sorts of (OAF . t) * ( the_arity_of o)) . w)

                      proof

                        

                         A36: y = ( commute ( commute y)) by WW, A28, FUNCT_6: 57;

                        let w be object;

                        reconsider Pi = (( the_arity_of o) /. w) as SortSymbol of S;

                        

                         A37: ( dom ( Carrier (OAF,(( the_arity_of o) /. w)))) = the carrier of P by PARTFUN1:def 2;

                        assume

                         A38: w in ( dom (the Sorts of (OAF . t) * ( the_arity_of o)));

                        then

                         A39: w in ( dom ( the_arity_of o)) by A33, FINSEQ_1:def 3;

                        (y . w) in ((MS * ( the_arity_of o)) . w) by A8, A14, A33, A34, A38, CARD_3: 9;

                        then

                         A40: (y . w) in (MS . (( the_arity_of o) . w)) by A39, FUNCT_1: 13;

                        reconsider y as Function-yielding Function by A36;

                        reconsider yw = (y . w) as Function;

                        (y . w) in (MS . (( the_arity_of o) /. w)) by A39, A40, PARTFUN1:def 6;

                        then yw in { ff where ff be Element of ( product ( Carrier (OAF,Pi))) : for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (ff . i)) = (ff . j) } by A1;

                        then ex jg be Element of ( product ( Carrier (OAF,Pi))) st jg = yw & for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (jg . i)) = (jg . j);

                        then

                         A41: (yw . t) in (( Carrier (OAF,(( the_arity_of o) /. w))) . t) by A37, CARD_3: 9;

                        ex U0 be MSAlgebra over S st U0 = (OAF . t) & (( Carrier (OAF,(( the_arity_of o) /. w))) . t) = (the Sorts of U0 . (( the_arity_of o) /. w)) by PRALG_2:def 9;

                        

                        then (( Carrier (OAF,(( the_arity_of o) /. w))) . t) = (the Sorts of (OAF . t) . (( the_arity_of o) . w)) by A39, PARTFUN1:def 6

                        .= ((the Sorts of (OAF . t) * ( the_arity_of o)) . w) by A39, FUNCT_1: 13;

                        hence thesis by A28, A33, A38, A41, FUNCT_6: 56;

                      end;

                      (Co . t) in ( rng Co) by A31, FUNCT_1:def 3;

                      then ex ts be Function st ts = (Co . t) & ( dom ts) = ( Seg ( len ( the_arity_of o))) & ( rng ts) c= |.OAF.| by A31, FUNCT_2:def 2;

                      hence thesis by A33, A35, CARD_3: 9;

                    end;

                    (( doms (OAF ?. o)) . t) = ( Args (o,(OAF . t))) by PRALG_2: 11;

                    hence thesis by A32, PRALG_2: 3;

                  end;

                  ( dom ( the_arity_of o)) <> {} by A29;

                  then ( Seg ( len ( the_arity_of o))) <> {} by FINSEQ_1:def 3;

                  then Co in ( Funcs (the carrier of P,( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)))) by A28, FUNCT_6: 55;

                  then

                  consider Co9 be Function such that

                   AA: Co9 = Co & ( dom Co9) = the carrier of P & ( rng Co9) c= ( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)) by FUNCT_2:def 2;

                  ( dom Co) = ( dom ( doms (OAF ?. o))) by AA, PRALG_2: 11;

                  then

                   A42: Co in ( product ( doms (OAF ?. o))) by A30, CARD_3: 9;

                  

                   A43: OPE = ( IFEQ (( the_arity_of o), {} ,( commute (OAF ?. o)),( Commute ( Frege (OAF ?. o))))) by PRALG_2:def 13;

                  then

                   A44: y in ( dom ( Commute ( Frege (OAF ?. o)))) by A11, A12, A29, FUNCOP_1:def 8;

                  reconsider y1 as Function;

                  

                   A45: ( dom (OAF ?. o)) = the carrier of P by PARTFUN1:def 2;

                  

                   S: ( dom Co) = the carrier of P by AA;

                  then i in (( dom (OAF ?. o)) /\ ( dom Co)) by A45;

                  then

                   a45: i in ( dom ((OAF ?. o) .. ( commute y))) by PRALG_1:def 19;

                  j in (( dom (OAF ?. o)) /\ ( dom Co)) by A45, S;

                  then

                   b45: j in ( dom ((OAF ?. o) .. ( commute y))) by PRALG_1:def 19;

                  

                   A46: x1 = (OPE . y) by A5, A6, A12, FUNCT_1: 47

                  .= (( Commute ( Frege (OAF ?. o))) . y) by A29, A43, FUNCOP_1:def 8

                  .= (( Frege (OAF ?. o)) . ( commute y)) by A44, PRALG_2:def 1

                  .= ((OAF ?. o) .. ( commute y)) by A42, PRALG_2:def 2;

                  

                  then

                   A47: (x1 . i) = (((OAF ?. o) . i) . (( commute y) . i)) by PRALG_1:def 19, a45

                  .= (( Den (o,(OAF . i))) . y1) by PRALG_2: 7;

                  ( dom ( the_arity_of o)) <> {} by A29;

                  then ( Seg ( len ( the_arity_of o))) <> {} by FINSEQ_1:def 3;

                  then Co in ( Funcs (the carrier of P,( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)))) by A28, FUNCT_6: 55;

                  then

                   A48: ex ss be Function st ss = Co & ( dom ss) = the carrier of P & ( rng ss) c= ( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)) by FUNCT_2:def 2;

                  y1 in ( product (the Sorts of (OAF . i) * ( the_arity_of o)))

                  proof

                    

                     A49: ( dom (the Sorts of (OAF . i) * ( the_arity_of o))) = ( dom ( the_arity_of o)) by PRALG_2: 3

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

                    

                     A50: for w be object st w in ( dom (the Sorts of (OAF . i) * ( the_arity_of o))) holds (y1 . w) in ((the Sorts of (OAF . i) * ( the_arity_of o)) . w)

                    proof

                      ( dom ( the_arity_of o)) <> {} by A29;

                      then ( Seg ( len ( the_arity_of o))) <> {} by FINSEQ_1:def 3;

                      then

                       A51: y = ( commute ( commute y)) by A28, FUNCT_6: 57;

                      let w be object;

                      reconsider Pi = (( the_arity_of o) /. w) as SortSymbol of S;

                      

                       A52: ( dom ( Carrier (OAF,(( the_arity_of o) /. w)))) = the carrier of P by PARTFUN1:def 2;

                      assume

                       A53: w in ( dom (the Sorts of (OAF . i) * ( the_arity_of o)));

                      then

                       A54: w in ( dom ( the_arity_of o)) by A49, FINSEQ_1:def 3;

                      w in ( dom y) by A16, A49, A53, FINSEQ_1:def 3;

                      then (y . w) in ((MS * ( the_arity_of o)) . w) by A8, A14, CARD_3: 9;

                      then

                       A55: (y . w) in (MS . (( the_arity_of o) . w)) by A54, FUNCT_1: 13;

                      reconsider y as Function-yielding Function by A51;

                      reconsider yw = (y . w) as Function;

                      (y . w) in (MS . (( the_arity_of o) /. w)) by A54, A55, PARTFUN1:def 6;

                      then yw in { ff where ff be Element of ( product ( Carrier (OAF,Pi))) : for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (ff . i)) = (ff . j) } by A1;

                      then ex jg be Element of ( product ( Carrier (OAF,Pi))) st jg = yw & for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (jg . i)) = (jg . j);

                      then

                       A56: (yw . i) in (( Carrier (OAF,(( the_arity_of o) /. w))) . i) by A52, CARD_3: 9;

                      ex U0 be MSAlgebra over S st U0 = (OAF . i) & (( Carrier (OAF,(( the_arity_of o) /. w))) . i) = (the Sorts of U0 . (( the_arity_of o) /. w)) by PRALG_2:def 9;

                      

                      then (( Carrier (OAF,(( the_arity_of o) /. w))) . i) = (the Sorts of (OAF . i) . (( the_arity_of o) . w)) by A54, PARTFUN1:def 6

                      .= ((the Sorts of (OAF . i) * ( the_arity_of o)) . w) by A54, FUNCT_1: 13;

                      hence thesis by A28, A49, A53, A56, FUNCT_6: 56;

                    end;

                    (Co . i) in ( rng Co) by A48, FUNCT_1:def 3;

                    then ex ts be Function st ts = (Co . i) & ( dom ts) = ( Seg ( len ( the_arity_of o))) & ( rng ts) c= |.OAF.| by A48, FUNCT_2:def 2;

                    hence thesis by A49, A50, CARD_3: 9;

                  end;

                  then

                  reconsider y19 = y1 as Element of ( Args (o,(OAF . i))) by PRALG_2: 3;

                  

                   A57: ( bind (B,i,j)) is_homomorphism ((OAF . i),(OAF . j)) by A13, Th2;

                  (( bind (B,i,j)) # y19) = (( commute y) . j)

                  proof

                    

                     A58: ( dom (( bind (B,i,j)) # y19)) = ( dom ( the_arity_of o)) by MSUALG_3: 6

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

                    then

                    reconsider One = (( bind (B,i,j)) # y19) as FinSequence by FINSEQ_1:def 2;

                    ( dom ( the_arity_of o)) <> {} by A29;

                    then

                     A59: ( Seg ( len ( the_arity_of o))) <> {} by FINSEQ_1:def 3;

                    then y = ( commute ( commute y)) by A28, FUNCT_6: 57;

                    then

                    reconsider y as Function-yielding Function;

                    reconsider y2 = (( commute y) . j) as Function;

                    Co in ( Funcs (the carrier of P,( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)))) by A28, A59, FUNCT_6: 55;

                    then

                     A60: ex ss be Function st ss = Co & ( dom ss) = the carrier of P & ( rng ss) c= ( Funcs (( Seg ( len ( the_arity_of o))), |.OAF.|)) by FUNCT_2:def 2;

                    then (Co . j) in ( rng Co) by FUNCT_1:def 3;

                    then

                     A61: ex ts be Function st ts = (Co . j) & ( dom ts) = ( Seg ( len ( the_arity_of o))) & ( rng ts) c= |.OAF.| by A60, FUNCT_2:def 2;

                    then

                    reconsider Two = y2 as FinSequence by FINSEQ_1:def 2;

                    

                     A62: (Co . i) in ( rng Co) by A60, FUNCT_1:def 3;

                    now

                      let n be Nat;

                      reconsider yn = (y . n) as Function;

                      reconsider Pi = (( the_arity_of o) /. n) as SortSymbol of S;

                      

                       A63: ex ts9 be Function st ts9 = (Co . i) & ( dom ts9) = ( Seg ( len ( the_arity_of o))) & ( rng ts9) c= |.OAF.| by A60, A62, FUNCT_2:def 2;

                      assume

                       A64: n in ( dom y2);

                      then

                       A65: (y . n) in ((MS * ( the_arity_of o)) . n) by A8, A14, A17, A61, CARD_3: 9;

                      

                       A66: n in ( dom ( the_arity_of o)) by A61, A64, FINSEQ_1:def 3;

                      then (( the_arity_of o) /. n) = (( the_arity_of o) . n) by PARTFUN1:def 6;

                      then yn in (MS . Pi) by A66, A65, FUNCT_1: 13;

                      then yn in { f where f be Element of ( product ( Carrier (OAF,Pi))) : for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (f . i)) = (f . j) } by A1;

                      then

                       A67: ex yn9 be Element of ( product ( Carrier (OAF,Pi))) st yn9 = yn & for i, j st i >= j holds ((( bind (B,i,j)) . Pi) . (yn9 . i)) = (yn9 . j);

                      (y19 . n) = (yn . i) by A28, A61, A64, FUNCT_6: 56;

                      

                      then ((( bind (B,i,j)) # y19) . n) = ((( bind (B,i,j)) . (( the_arity_of o) /. n)) . (yn . i)) by A61, A64, A63, MSUALG_3:def 6

                      .= (yn . j) by A13, A67;

                      hence ((( bind (B,i,j)) # y19) . n) = (y2 . n) by A28, A61, A64, FUNCT_6: 56;

                    end;

                    then for n be Nat st n in ( Seg ( len ( the_arity_of o))) holds (One . n) = (Two . n) by A61;

                    hence thesis by A61, A58, FINSEQ_1: 13;

                  end;

                  

                  then (( Den (o,(OAF . j))) . (( bind (B,i,j)) # y19)) = (((OAF ?. o) . j) . (( commute y) . j)) by PRALG_2: 7

                  .= (x1 . j) by A46, PRALG_1:def 19, b45;

                  hence thesis by A57, A47, MSUALG_3:def 7;

                end;

                  suppose

                   A68: ( the_arity_of o) = {} ;

                  reconsider co = (( commute (OAF ?. o)) . y) as Function;

                  

                   A69: (MS * {} ) = {} ;

                  

                   A70: co = (( curry' ( uncurry (OAF ?. o))) . y) by FUNCT_6:def 10;

                  

                   A71: ( dom (OAF ?. o)) = the carrier of P by PARTFUN1:def 2;

                  

                   A72: ( Den (o,( product OAF))) = (the Charact of ( product OAF) . o) by MSUALG_1:def 6

                  .= (( OPS OAF) . o) by PRALG_2: 12

                  .= ( IFEQ (( the_arity_of o), {} ,( commute (OAF ?. o)),( Commute ( Frege (OAF ?. o))))) by PRALG_2:def 13

                  .= ( commute (OAF ?. o)) by A68, FUNCOP_1:def 8;

                  

                   A73: for d be Element of P holds (x1 . d) = (( Den (o,(OAF . d))) . {} )

                  proof

                    reconsider co9 = (( curry' ( uncurry (OAF ?. o))) . y) as Function by A70;

                    let d be Element of P;

                    reconsider g = ((OAF ?. o) . d) as Function;

                    

                     A74: x1 = (( commute (OAF ?. o)) . y) by A5, A6, A72, FUNCT_1: 47;

                    g = ( Den (o,(OAF . d))) by PRALG_2: 7;

                    

                    then ( dom g) = ( Args (o,(OAF . d))) by FUNCT_2:def 1

                    .= { {} } by A68, PRALG_2: 4;

                    then

                     A75: y in ( dom g) by A8, A68, CARD_3: 10;

                    then

                     A76: [d, y] in ( dom ( uncurry (OAF ?. o))) by A71, FUNCT_5: 38;

                    (co . d) = (co9 . d) by FUNCT_6:def 10

                    .= (( uncurry (OAF ?. o)) . (d,y)) by A76, FUNCT_5: 22

                    .= (g . y) by A71, A75, FUNCT_5: 38;

                    

                    then (x1 . d) = (( Den (o,(OAF . d))) . y) by A74, PRALG_2: 7

                    .= (( Den (o,(OAF . d))) . {} ) by A8, A68, A69, CARD_3: 10, TARSKI:def 1;

                    hence thesis;

                  end;

                  then

                   A77: (x1 . i) = (( Den (o,(OAF . i))) . {} );

                  ( Args (o,(OAF . i))) = { {} } by A68, PRALG_2: 4;

                  then

                  reconsider E = {} as Element of ( Args (o,(OAF . i))) by TARSKI:def 1;

                  set F = ( bind (B,i,j));

                  

                   A78: ( Args (o,(OAF . j))) = { {} } by A68, PRALG_2: 4;

                  ( bind (B,i,j)) is_homomorphism ((OAF . i),(OAF . j)) by A13, Th2;

                  then

                   A79: ((F . ( the_result_sort_of o)) . (x1 . i)) = (( Den (o,(OAF . j))) . (F # E)) by A77, MSUALG_3:def 7;

                  (x1 . j) = (( Den (o,(OAF . j))) . {} ) by A73;

                  hence thesis by A79, A78, TARSKI:def 1;

                end;

              end;

              then x in { f where f be Element of ( product ( Carrier (OAF,( the_result_sort_of o)))) : for i, j st i >= j holds ((( bind (B,i,j)) . ( the_result_sort_of o)) . (f . i)) = (f . j) } by A10;

              hence x in (C . ( the_result_sort_of o)) by A1;

            end;

            then x in (C . ( the_result_sort_of o));

            then

             A80: x in (C . (the ResultSort of S . o)) by MSUALG_1:def 2;

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

            hence thesis by A80, FUNCT_1: 13;

          end;

          hence thesis by MSUALG_2:def 5;

        end;

        then

         A81: C is opers_closed by MSUALG_2:def 6;

        reconsider C as MSSubset of L;

        set MSA = (L | C);

        

         A82: MSA = MSAlgebra (# C, ( Opers (L,C)) #) by A81, MSUALG_2:def 15;

        now

          let s be SortSymbol of S;

          let f be Element of (( SORTS OAF) . s);

          

           A83: f is Element of ( product ( Carrier (OAF,s))) by PRALG_2:def 10;

          thus f in (the Sorts of MSA . s) iff for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j)

          proof

            hereby

              assume f in (the Sorts of MSA . s);

              then f in { g where g be Element of ( product ( Carrier (OAF,s))) : for i, j st i >= j holds ((( bind (B,i,j)) . s) . (g . i)) = (g . j) } by A1, A82;

              then ex k be Element of ( product ( Carrier (OAF,s))) st k = f & for i, j st i >= j holds ((( bind (B,i,j)) . s) . (k . i)) = (k . j);

              hence for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j);

            end;

            assume for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j);

            then f in { h where h be Element of ( product ( Carrier (OAF,s))) : for i, j st i >= j holds ((( bind (B,i,j)) . s) . (h . i)) = (h . j) } by A83;

            hence thesis by A1, A82;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let A1,A2 be strict MSSubAlgebra of ( product OAF) such that

         A84: for s be SortSymbol of S holds for f be Element of (( SORTS OAF) . s) holds f in (the Sorts of A1 . s) iff for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j) and

         A85: for s be SortSymbol of S holds for f be Element of (( SORTS OAF) . s) holds f in (the Sorts of A2 . s) iff for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j);

        for s be object st s in the carrier of S holds (the Sorts of A1 . s) = (the Sorts of A2 . s)

        proof

          let a be object;

          assume a in the carrier of S;

          then

          reconsider s = a as SortSymbol of S;

          thus (the Sorts of A1 . a) c= (the Sorts of A2 . a)

          proof

            let e be object;

            assume

             A86: e in (the Sorts of A1 . a);

            the Sorts of A1 is MSSubset of ( product OAF) by MSUALG_2:def 9;

            then the Sorts of A1 c= the Sorts of ( product OAF) by PBOOLE:def 18;

            then the Sorts of A1 c= ( SORTS OAF) by PRALG_2: 12;

            then (the Sorts of A1 . s) c= (( SORTS OAF) . s) by PBOOLE:def 2;

            then

            reconsider f = e as Element of (( SORTS OAF) . s) by A86;

            for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j) by A84, A86;

            hence thesis by A85;

          end;

          let e be object;

          assume

           A87: e in (the Sorts of A2 . a);

          the Sorts of A2 is MSSubset of ( product OAF) by MSUALG_2:def 9;

          then the Sorts of A2 c= the Sorts of ( product OAF) by PBOOLE:def 18;

          then the Sorts of A2 c= ( SORTS OAF) by PRALG_2: 12;

          then (the Sorts of A2 . s) c= (( SORTS OAF) . s) by PBOOLE:def 2;

          then

          reconsider f = e as Element of (( SORTS OAF) . s) by A87;

          for i, j st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j) by A85, A87;

          hence thesis by A84;

        end;

        hence thesis by MSUALG_2: 9, PBOOLE: 3;

      end;

    end

    theorem :: MSALIMIT:5

    for DP be discrete non empty Poset, S holds for OAF be OrderedAlgFam of DP, S holds for B be normalized Binding of OAF holds ( InvLim B) = ( product OAF)

    proof

      let DP be discrete non empty Poset, S;

      let OAF be OrderedAlgFam of DP, S;

      let B be normalized Binding of OAF;

      

       A1: for s be object st s in the carrier of S holds (the Sorts of ( InvLim B) . s) = (the Sorts of ( product OAF) . s)

      proof

        let a be object;

        assume a in the carrier of S;

        then

        reconsider s = a as SortSymbol of S;

        thus (the Sorts of ( InvLim B) . a) c= (the Sorts of ( product OAF) . a)

        proof

          let e be object;

          the Sorts of ( InvLim B) is MSSubset of ( product OAF) by MSUALG_2:def 9;

          then the Sorts of ( InvLim B) c= the Sorts of ( product OAF) by PBOOLE:def 18;

          then

           A2: (the Sorts of ( InvLim B) . s) c= (the Sorts of ( product OAF) . s) by PBOOLE:def 2;

          assume e in (the Sorts of ( InvLim B) . a);

          hence thesis by A2;

        end;

        let e be object;

        assume e in (the Sorts of ( product OAF) . a);

        then

        reconsider f = e as Element of (( SORTS OAF) . s) by PRALG_2: 12;

        for i,j be Element of DP st i >= j holds ((( bind (B,i,j)) . s) . (f . i)) = (f . j)

        proof

          let i,j be Element of DP;

          assume i >= j;

          then

           A3: i = j by ORDERS_3: 1;

          f in (( SORTS OAF) . s);

          then ( dom ( Carrier (OAF,s))) = the carrier of DP & f in ( product ( Carrier (OAF,s))) by PARTFUN1:def 2, PRALG_2:def 10;

          then

           A4: (f . i) in (( Carrier (OAF,s)) . i) by CARD_3: 9;

          ( bind (B,i,i)) = (B . (i,i)) by Def3, ORDERS_2: 1

          .= ( id the Sorts of (OAF . i)) by Def4;

          then

           A5: (( bind (B,i,i)) . s) = ( id (the Sorts of (OAF . i) . s)) by MSUALG_3:def 1;

          ex U0 be MSAlgebra over S st U0 = (OAF . i) & (( Carrier (OAF,s)) . i) = (the Sorts of U0 . s) by PRALG_2:def 9;

          hence thesis by A3, A5, A4, FUNCT_1: 18;

        end;

        hence thesis by Def6;

      end;

      ( product OAF) is MSSubAlgebra of ( product OAF) by MSUALG_2: 5;

      hence thesis by A1, MSUALG_2: 9, PBOOLE: 3;

    end;

    begin

    reserve x for set,

A for non empty set;

    definition

      let X be set;

      :: MSALIMIT:def7

      attr X is MSS-membered means

      : Def7: x in X implies x is strict non empty non void ManySortedSign;

    end

    registration

      cluster non empty MSS-membered for set;

      existence

      proof

        set S = the strict non empty non void ManySortedSign;

        set A = {S};

        for x be set st x in A holds x is strict non empty non void ManySortedSign by TARSKI:def 1;

        then A is MSS-membered;

        hence thesis;

      end;

    end

    registration

      cluster strict empty void for ManySortedSign;

      existence

      proof

        ( dom ( {} --> {} )) = {} & ( rng ( {} --> {} )) = {} ;

        then

        reconsider g = ( {} --> {} ) as Function of {} , {} by RELSET_1: 4;

         {} in ( {} * ) by FINSEQ_1: 49;

        then

        reconsider f = ( {} --> {} ) as Function of {} , ( {} * ) by FUNCOP_1: 46;

        take ManySortedSign (# {} , {} , f, g #);

        thus thesis;

      end;

    end

    

     Lm1: for S be empty void ManySortedSign holds (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S)

    proof

      let S be empty void ManySortedSign;

      set f = ( id the carrier of S);

      ( {} * the ResultSort of S) = (the ResultSort of S * {} ) & for o be set, p be Function st o in the carrier' of S & p = (the Arity of S . o) holds (f * p) = (the Arity of S . (f . o));

      hence thesis by PUA2MSS1:def 12, RELAT_1: 38;

    end;

    

     Lm2: for S be non empty void ManySortedSign holds (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S)

    proof

      let S be non empty void ManySortedSign;

      set f = ( id the carrier of S), g = ( id the carrier' of S);

      

       A1: ( rng f) c= the carrier of S & ( rng g) c= the carrier' of S;

      

       A2: (f * the ResultSort of S) = {} & (the ResultSort of S * g) = {} ;

      

       A3: for o be set, p be Function st o in the carrier' of S & p = (the Arity of S . o) holds (f * p) = (the Arity of S . (g . o));

      ( dom f) = the carrier of S & ( dom g) = the carrier' of S;

      hence thesis by A1, A2, A3, PUA2MSS1:def 12;

    end;

    theorem :: MSALIMIT:6

    for S be void ManySortedSign holds (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S)

    proof

      let S be void ManySortedSign;

      per cases ;

        suppose S is empty;

        hence thesis by Lm1;

      end;

        suppose S is non empty;

        hence thesis by Lm2;

      end;

    end;

    definition

      ::$Canceled

      let A;

      :: MSALIMIT:def9

      func MSS_set A -> set means

      : Def8: for x be object holds x in it iff ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A;

      existence

      proof

        defpred P[ object, object] means ex S be strict non empty non void ManySortedSign st S = $2 & $1 = [the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S];

        

         A1: for x,y,z be object st P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object;

          assume P[x, y] & P[x, z];

          then

          consider S1,S2 be strict non empty non void ManySortedSign such that

           A2: S1 = y and

           A3: x = [the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1] and

           A4: S2 = z and

           A5: x = [the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2] and S2 is empty implies S2 is void;

          

           A6: the Arity of S1 = the Arity of S2 by A3, A5, XTUPLE_0: 5;

          the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 by A3, A5, XTUPLE_0: 5;

          hence thesis by A2, A3, A4, A5, A6, XTUPLE_0: 5;

        end;

        consider X be set such that

         A7: for x be object holds x in X iff ex y be object st y in [:( bool A), ( bool A), ( PFuncs (A,(A * ))), ( PFuncs (A,A)):] & P[y, x] from TARSKI:sch 1( A1);

        take X;

        let x be object;

        thus x in X iff ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A

        proof

          thus x in X implies ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A

          proof

            assume x in X;

            then

            consider y be object such that

             A8: y in [:( bool A), ( bool A), ( PFuncs (A,(A * ))), ( PFuncs (A,A)):] and

             A9: P[y, x] by A7;

            consider S be strict non empty non void ManySortedSign such that

             A10: S = x and y = [the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S] by A9;

            take S;

            the carrier of S in ( bool A) & the carrier' of S in ( bool A) by A8, A9, A10, MCART_1: 80;

            hence thesis by A10;

          end;

          given S be strict non empty non void ManySortedSign such that

           A11: x = S and

           A12: the carrier of S c= A and

           A13: the carrier' of S c= A;

          ( dom the ResultSort of S) = the carrier' of S & ( rng the ResultSort of S) c= A by A12, FUNCT_2:def 1;

          then

           A14: the ResultSort of S in ( PFuncs (A,A)) by A13, PARTFUN1:def 3;

          reconsider C = the carrier of S as Subset of A by A12;

          consider y be set such that

           A15: y = [the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S];

          (C * ) c= (A * ) by MSUHOM_1: 2;

          then

           A16: ( rng the Arity of S) c= (A * );

          ( dom the Arity of S) c= A by A13;

          then the Arity of S in ( PFuncs (A,(A * ))) by A16, PARTFUN1:def 3;

          then y in [:( bool A), ( bool A), ( PFuncs (A,(A * ))), ( PFuncs (A,A)):] by A12, A13, A15, A14, MCART_1: 80;

          hence thesis by A7, A11, A15;

        end;

      end;

      uniqueness

      proof

        let A1,A2 be set such that

         A17: for x be object holds x in A1 iff ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A and

         A18: for x be object holds x in A2 iff ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A;

        thus A1 c= A2

        proof

          let x be object;

          assume x in A1;

          then ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A by A17;

          hence thesis by A18;

        end;

        thus A2 c= A1

        proof

          let x be object;

          assume x in A2;

          then ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A by A18;

          hence thesis by A17;

        end;

      end;

    end

    registration

      let A;

      cluster ( MSS_set A) -> non empty MSS-membered;

      coherence

      proof

        set X = ( MSS_set A);

        set a = the Element of A;

        ( dom ( {a} --> a)) = {a} & ( rng ( {a} --> a)) c= {a} by FUNCOP_1: 13;

        then

        reconsider g = ( {a} --> a) as Function of {a}, {a} by FUNCT_2: 2;

        a in {a} by TARSKI:def 1;

        then <*a*> in ( {a} * ) by FUNCT_7: 18;

        then

        reconsider f = ( {a} --> <*a*>) as Function of {a}, ( {a} * ) by FUNCOP_1: 46;

        

         A1: {a} c= A by ZFMISC_1: 31;

         ManySortedSign (# {a}, {a}, f, g #) in X

        proof

          set SI = ManySortedSign (# {a}, {a}, f, g #);

          SI is non void non empty;

          hence thesis by A1, Def8;

        end;

        hence X is non empty;

        thus X is MSS-membered

        proof

          let x be set;

          assume x in X;

          then ex S be strict non empty non void ManySortedSign st x = S & the carrier of S c= A & the carrier' of S c= A by Def8;

          hence thesis;

        end;

      end;

    end

    definition

      let A be non empty MSS-membered set;

      :: original: Element

      redefine

      mode Element of A -> strict non empty non void ManySortedSign ;

      coherence by Def7;

    end

    definition

      let S1,S2 be ManySortedSign;

      :: MSALIMIT:def10

      func MSS_morph (S1,S2) -> set means x in it iff ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2);

      existence

      proof

        defpred P[ object] means ex f,g be Function st $1 = [f, g] & (f,g) form_morphism_between (S1,S2);

        consider X be set such that

         A1: for x be object holds x in X iff x in [:( PFuncs (the carrier of S1,the carrier of S2)), ( PFuncs (the carrier' of S1,the carrier' of S2)):] & P[x] from XBOOLE_0:sch 1;

        take X;

        thus x in X iff ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2)

        proof

          thus x in X implies ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2) by A1;

          given f,g be Function such that

           A2: x = [f, g] and

           A3: (f,g) form_morphism_between (S1,S2);

          ( dom g) = the carrier' of S1 & ( rng g) c= the carrier' of S2 by A3, PUA2MSS1:def 12;

          then

           A4: g in ( PFuncs (the carrier' of S1,the carrier' of S2)) by PARTFUN1:def 3;

          ( dom f) = the carrier of S1 & ( rng f) c= the carrier of S2 by A3, PUA2MSS1:def 12;

          then f in ( PFuncs (the carrier of S1,the carrier of S2)) by PARTFUN1:def 3;

          then x in [:( PFuncs (the carrier of S1,the carrier of S2)), ( PFuncs (the carrier' of S1,the carrier' of S2)):] by A2, A4, ZFMISC_1: 87;

          hence thesis by A1, A2, A3;

        end;

      end;

      uniqueness

      proof

        let A1,A2 be set;

        assume that

         A5: x in A1 iff ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2) and

         A6: x in A2 iff ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2);

        

         A7: A2 c= A1

        proof

          let x be object;

          assume x in A2;

          then ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2) by A6;

          hence thesis by A5;

        end;

        A1 c= A2

        proof

          let x be object;

          assume x in A1;

          then ex f,g be Function st x = [f, g] & (f,g) form_morphism_between (S1,S2) by A5;

          hence thesis by A6;

        end;

        hence A1 = A2 by A7;

      end;

    end