:: Inverse Limits of Many Sorted Algebras
::  by Adam Grabowski
::
:: Received June 11, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ORDERS_2, SUBSET_1, STRUCT_0, MSUALG_1, PRALG_2,
      FUNCT_1, RELAT_1, CARD_3, RLVECT_2, PBOOLE, XXREAL_0, MEMBER_1, MSUALG_3,
      FUNCOP_1, RELAT_2, MCART_1, MSUALG_2, TARSKI, UNIALG_2, MARGREL1,
      FUNCT_6, FINSEQ_1, FUNCT_2, COMPLEX1, PARTFUN1, FINSEQ_4, NAT_1, FUNCT_5,
      NATTRA_1, PUA2MSS1, ZFMISC_1, MSALIMIT;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XTUPLE_0, MCART_1,
      RELAT_1, FUNCT_1, STRUCT_0, RELAT_2, FUNCT_2, FINSEQ_1, FINSEQ_2,
      ORDERS_2, FUNCOP_1, RELSET_1, PARTFUN1, CARD_3, BINOP_1, FUNCT_5,
      FUNCT_6, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, PRALG_2,
      PUA2MSS1, ORDERS_3;
 constructors PRALG_1, PRALG_2, MSUALG_3, PUA2MSS1, ORDERS_3, RELSET_1,
      FUNCT_5, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE,
      STRUCT_0, ORDERS_2, MSUALG_1, MSUALG_2, PRALG_2, MSUALG_3, ORDERS_3,
      PRALG_3, ORDINAL1, CARD_3, RELSET_1, FINSEQ_1, XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, BINOP_1, XTUPLE_0;
 theorems ALTCAT_1, CARD_3, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCT_5,
      FUNCT_7, MCART_1, MSUALG_1, MSUALG_2, MSUALG_3, MSUHOM_1, ORDERS_2,
      ORDERS_3, PARTFUN1, PBOOLE, PRALG_1, PRALG_2, PUA2MSS1, RELAT_1, RELAT_2,
      TARSKI, ZFMISC_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDERS_1, FUNCT_6,
      FINSEQ_2, XTUPLE_0;
 schemes FRAENKEL, PBOOLE, TARSKI, XBOOLE_0;

begin :: Inverse Limits of Many Sorted Algebras

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 being 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;
  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 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 set 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;
A1: Z.j = A by FUNCOP_1:7;
    Z.k = A by FUNCOP_1:7;
    then consider F2 be ManySortedFunction of Z.j, Z.k such that
A2: F2 = id (the Sorts of A) by A1;
    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;
A5: Z.i = A by FUNCOP_1:7;
    then consider F1 be ManySortedFunction of Z.i, Z.j such that
A6: F1 = id (the Sorts of A) by A1;
    take F1;
    take F2;
    F2 ** F1 = id (the Sorts of A) by A6,A2,MSUALG_3:3;
    hence thesis by A3,A5,A1,A6,A2,A4,FUNCOP_1:7,MSUALG_3:9;
  end;
end;

reserve OAF for OrderedAlgFam of P, S;

definition
  let P, S, OAF;
  mode Binding of OAF -> ManySortedFunction of the InternalRel of P means
    :
    Def2: for
 i,j,k st i >= j & j >= k 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;
  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 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;
  attr IT is normalized means
  :Def4:
  for i holds IT.(i,i) = id (the Sorts of OAF.i);
end;

theorem Th2:
  for P,S,OAF,B,i,j st i >= j 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;
  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[set,set] 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) );
    now
      let ij be set;
      assume
A1:   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(set)= 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
A2:   for ij be set 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 A1,A2,MCART_1:21;
    end;
    then
A3: for z being set st z in the InternalRel of P ex y being set st P[z,y];
    consider A be ManySortedSet of the InternalRel of P such that
A4: for ij being set st ij in the InternalRel of P holds P[ij,A.ij]
    from PBOOLE:sch 3(A3);
    for z be set st z in dom A holds A.z is Function
    proof
      let z be set;
      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
A5:   A.z = IFEQ (i2, i1, id (the Sorts of OAF.i1), bind (B,i1,i2) **
      id (the Sorts of OAF.i1) ) by A4;
      per cases;
      suppose
        i1 = i2;
        hence thesis by A5,FUNCOP_1:def 8;
      end;
      suppose
        i1 <> i2;
        hence thesis by A5,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
A6:   i >= j and
A7:   j >= k;
      consider kl be set such that
A8:   kl = [j,i];
      kl in the InternalRel of P by A6,A8,ORDERS_2:def 5;
      then consider i1,j1 be Element of P such that
A9:   [j1,i1] = kl and
A10:  A.kl = IFEQ (j1, i1, id (the Sorts of OAF.i1), bind (B,i1,j1)
      ** id (the Sorts of OAF.i1) ) by A4;
A11:  i1 = i & j1 = j by A8,A9,XTUPLE_0:1;
      A.(j,i) is ManySortedFunction of OAF.i,OAF.j
      proof
        per cases;
        suppose
          i = j;
          hence thesis by A9,A10,A11,FUNCOP_1:def 8;
        end;
        suppose
          i <> j;
          hence thesis by A9,A10,A11,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
A12:  lm = [k,j];
      lm in the InternalRel of P by A7,A12,ORDERS_2:def 5;
      then consider i2,j2 be Element of P such that
A13:  [j2,i2] = lm and
A14:  A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
      ** id (the Sorts of OAF.i2) ) by A4;
A15:  j2 = k & i2 = j by A12,A13,XTUPLE_0:1;
      A.(k,j) is ManySortedFunction of OAF.j,OAF.k
      proof
        per cases;
        suppose
          j = k;
          hence thesis by A13,A14,A15,FUNCOP_1:def 8;
        end;
        suppose
          j <> k;
          hence thesis by A13,A14,A15,FUNCOP_1:def 8;
        end;
      end;
      then reconsider f2 = A.(k,j) as ManySortedFunction of OAF.j,OAF.k;
A16:  for i,j st i >= j & i <> j holds A.(j,i) = bind (B,i,j)
      proof
        let i,j;
        assume that
A17:    i >= j and
A18:    i <> j;
        consider lm be set such that
A19:    lm = [j,i];
        lm in the InternalRel of P by A17,A19,ORDERS_2:def 5;
        then consider i2,j2 be Element of P such that
A20:    [j2,i2] = lm and
A21:    A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
        ** id (the Sorts of OAF.i2) ) by A4;
        i2 = i & j2 = j by A19,A20,XTUPLE_0:1;
        then
        A.(j,i) = bind (B,i,j) ** id (the Sorts of OAF.i) by A18,A20,A21,
FUNCOP_1:def 8;
        hence thesis by MSUALG_3:3;
      end;
A22:  A.(k,i) = f2 ** f1
      proof
        per cases;
        suppose
A23:      i = j & j = k;
          then f2 = id (the Sorts of OAF.j) by A13,A14,A15,FUNCOP_1:def 8;
          hence thesis by A23,MSUALG_3:3;
        end;
        suppose
A24:      i = j & j <> k;
          then f1 = id (the Sorts of OAF.i) by A9,A10,A11,FUNCOP_1:def 8;
          hence thesis by A24,MSUALG_3:3;
        end;
        suppose
A25:      i <> j & j = k;
          then f2 = id (the Sorts of OAF.j) by A13,A14,A15,FUNCOP_1:def 8;
          hence thesis by A25,MSUALG_3:4;
        end;
        suppose
A26:      i <> j & j <> k;
          then i > j & j > k by A6,A7,ORDERS_2:def 6;
          then
A27:      i <> k by ORDERS_2:5;
          f2 = bind (B,j,k) ** id (the Sorts of OAF.j) by A13,A14,A15,A26,
FUNCOP_1:def 8;
          then
A28:      f2 = bind (B,j,k) by MSUALG_3:3;
          f1 = bind (B,i,j) ** id (the Sorts of OAF.i) by A9,A10,A11,A26,
FUNCOP_1:def 8;
          then f1 = bind (B,i,j) by MSUALG_3:3;
          then f2 ** f1 = bind (B,i,k) by A6,A7,A28,Th1;
          hence thesis by A6,A7,A16,A27,ORDERS_2:3;
        end;
      end;
A29:  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
A30:    lm = [j,i];
        assume
A31:    i = j;
        then i >= j by ORDERS_2:1;
        then lm in the InternalRel of P by A30,ORDERS_2:def 5;
        then consider i2,j2 be Element of P such that
A32:    [j2,i2] = lm and
A33:    A.lm = IFEQ (j2, i2, id (the Sorts of OAF.i2), bind (B,i2,j2)
        ** id (the Sorts of OAF.i2) ) by A4;
        i2 = i & j2 = j by A30,A32,XTUPLE_0:1;
        hence thesis by A31,A32,A33,FUNCOP_1:def 8;
      end;
      f1 is_homomorphism OAF.i, OAF.j
      proof
        per cases;
        suppose
A34:      i = j;
          then A.(i,j) = id (the Sorts of OAF.i) by A29;
          hence thesis by A34,MSUALG_3:9;
        end;
        suppose
          i <> j;
          then A.(j,i) = bind (B,i,j) by A6,A16;
          hence thesis by A6,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 A22;
    end;
    then reconsider A as Binding of OAF by Def2;
    take A;
    let i, j;
    consider kl be set such that
A35: kl = [j,i];
    assume i >= j;
    then kl in the InternalRel of P by A35,ORDERS_2:def 5;
    then consider i1,j1 be Element of P such that
A36: [j1,i1] = kl and
A37: A.kl = IFEQ (j1, i1, id (the Sorts of OAF.i1), bind (B,i1,j1) **
    id (the Sorts of OAF.i1) ) by A4;
    i1 = i & j1 = j by A35,A36,XTUPLE_0:1;
    hence thesis by A36,A37;
  end;
  uniqueness
  proof
    let N1, N2 be Binding of OAF such that
A38: 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
A39: 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 set;
      assume
A40:  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;
A41:  N2.ij = N2.(i2,i1) by A40,MCART_1:21;
      ij = [ij`1,ij`2] by A40,MCART_1:21;
      then
A42:  i2 <= i1 by A40,ORDERS_2:def 5;
      N1.ij = N1.(i2,i1) by A40,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 A38,A42;
      hence N1.ij = N2.ij by A39,A42,A41;
    end;
    hence N1 = N2 by PBOOLE:3;
  end;
end;

theorem 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
  for NB be normalized Binding of OAF 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;
  func InvLim B -> strict MSSubAlgebra of product OAF means
  :Def6:
  for s be
SortSymbol of S 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 is 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 set st i in the carrier of S holds C.i c= (SORTS OAF).i
    proof
      let i be set;
      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 is 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 set;
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 set 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 set;
              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 set;
              assume z in rng y;
              then consider n be set 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 is 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 set;
                assume p in rng z;
                then consider r be set 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 {|.OAF.k.| where k is Element of P:not
                contradiction};
                then |.OAF.r9.| c= union {|.OAF.k.| where k is Element
 of P: not contradiction} 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 set st t in dom doms(OAF?.o) holds Co.t in (doms(
              OAF?.o)).t
              proof
                let t be set;
                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 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 set 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
                    dom (the_arity_of o) <> {} by A29;
                    then Seg len (the_arity_of o) <> {} by FINSEQ_1:def 3;
                    then
A36:                y = commute commute y by A28,FUNCT_6:57;
                    let w be set;
                    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 is 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;
A42:          Co in product doms (OAF?.o)
              proof
                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 ex Co9 be Function st Co9 = Co & dom Co9 = the carrier of
P & rng Co9 c= Funcs(Seg len (the_arity_of o),|.OAF.|) by FUNCT_2:def 2;
                then dom Co = dom doms (OAF?.o) by PRALG_2:11;
                hence thesis by A30,CARD_3:9;
              end;
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;
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 A45,PRALG_1:def 17
                .= (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 set 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 set;
                  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 is 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 is 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 A45,A46,PRALG_1:def 17;
              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 is 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 is 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 is 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 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 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 set st s in the carrier of S holds (the Sorts of A1).s = (
    the Sorts of A2).s
    proof
      let a be set;
      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 set;
        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 set;
      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
  for DP be discrete non empty Poset, S for OAF be OrderedAlgFam of DP,S
  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 set st s in the carrier of S holds (the Sorts of InvLim B).s =
  (the Sorts of product OAF).s
  proof
    let a be set;
    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 set;
      (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 set;
    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 being 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  :: Sets and Morphisms of Many Sorted Signatures

reserve x for set,
  A for non empty set;

definition
  let X be set;
  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 by Def7;
    hence thesis;
  end;
end;

definition
  func TrivialMSSign -> strict ManySortedSign means
  :Def8:
  it is empty void;
  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;
  uniqueness
  proof
    let C1, C2 be strict ManySortedSign;
    assume that
A1: C1 is empty void and
A2: C2 is empty void;
    C1 = C2
    proof
A3:   the carrier of C1 = {} & the carrier' of C1 = {} by A1;
      then reconsider RS = the ResultSort of C1, RT = the ResultSort of C2 as
      Function of {},{} by A2;
A4:   the carrier of C2 = {} & the carrier' of C2 = {} by A2;
A5:   RT in { id {} } by ALTCAT_1:2,FUNCT_2:9;
      RS in { id {} } by ALTCAT_1:2,FUNCT_2:9;
      then the ResultSort of C1 = id {} .= the ResultSort of C2 by A5;
      hence thesis by A3,A4;
    end;
    hence thesis;
  end;
end;

registration
  cluster TrivialMSSign -> empty void;
  coherence by Def8;
end;

registration
  cluster strict empty void for ManySortedSign;
  existence
  proof
    take TrivialMSSign;
    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
  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
  let A;
  func MSS_set A means
  :Def9:
  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[set,set] 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 set st P[x,y] & P[x,z] holds y = z
    proof
      let x,y,z be set;
      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 holds x in X iff ex y be set 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 set;
    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 set 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,XBOOLE_1: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* by XBOOLE_1:1;
      dom the Arity of S c= A by A13,FUNCT_2:def 1;
      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: 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: 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 set;
      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 set;
      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,Def9;
    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 Def9;
      hence thesis;
    end;
  end;
end;

definition
  let A be non empty MSS-membered set;
  redefine mode Element of A -> strict non empty non void ManySortedSign;
  coherence by Def7;
end;

definition
  let S1,S2 be ManySortedSign;
  func MSS_morph (S1,S2) 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[set] means ex f,g be Function st $1 = [f,g] & f,g
    form_morphism_between S1,S2;
    consider X be set such that
A1: 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;
      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;
      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,XBOOLE_0:def 10;
  end;
end;