The Mizar article:

On the Trivial Many Sorted Algebras and Many Sorted Congruences

by
Artur Kornilowicz

Received June 11, 1996

Copyright (c) 1996 Association of Mizar Users

MML identifier: MSUALG_9
[ MML identifier index ]


environ

 vocabulary AMI_1, MSUALG_1, PBOOLE, FUNCT_1, PRE_CIRC, CLOSURE2, CAT_4,
      MSUALG_2, ZF_REFLE, FINSET_1, FINSEQ_1, RELAT_1, QC_LANG1, PRALG_2,
      CARD_3, RLVECT_2, MSAFREE, PRELAMB, PRALG_1, FUNCT_3, MCART_1, EQREL_1,
      FUNCOP_1, BOOLE, MSUALG_3, TREES_4, LANG1, BORSUK_1, ALG_1, GROUP_6,
      WELLORD1, TDGROUP, FINSEQ_4, NATTRA_1, FUNCT_6, MSUALG_4, MSUALG_5,
      SETFAM_1, FUNCT_4, CANTOR_1, RELAT_2, MSUALG_9;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
      RELAT_2, STRUCT_0, SETFAM_1, RELSET_1, FUNCT_1, EQREL_1, FUNCT_2,
      FINSEQ_1, LANG1, MCART_1, FINSET_1, CARD_3, FINSEQ_4, CANTOR_1, TREES_4,
      DTCONSTR, PBOOLE, MSUALG_1, MSUALG_2, PRALG_3, MSUALG_3, MSAFREE,
      PRALG_2, PRE_CIRC, MSAFREE2, MSUALG_4, AUTALG_1, EXTENS_1, PZFMISC1,
      MSSUBFAM, CLOSURE1, CLOSURE2, MSUALG_5;
 constructors AUTALG_1, BINOP_1, CANTOR_1, CLOSURE1, CLOSURE2, EXTENS_1,
      MSAFREE2, MSUALG_5, PRALG_3, PRE_CIRC, PZFMISC1, FINSEQ_4;
 clusters CANTOR_1, CLOSURE2, EQREL_1, FINSET_1, MSAFREE, MSSUBFAM, MSUALG_1,
      MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5, PRALG_1, PRALG_2, PRE_CIRC,
      PZFMISC1, RELSET_1, STRUCT_0, ARYTM_3, XBOOLE_0, MEMBERED, PARTFUN1,
      NUMBERS, ORDINAL2;
 requirements SUBSET, BOOLE;
 definitions AUTALG_1, FINSEQ_1, FUNCT_1, MSAFREE2, MSUALG_1, MSUALG_2,
      MSUALG_3, MSUALG_4, PBOOLE, PRE_CIRC, TARSKI, XBOOLE_0;
 theorems AUTALG_1, CANTOR_1, CARD_3, CLOSURE1, CLOSURE2, DTCONSTR, EXTENS_1,
      EQREL_1, FINSEQ_1, FUNCOP_1, FUNCT_1, FUNCT_2, MCART_1, MSAFREE,
      MSAFREE2, MSSUBFAM, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_5,
      MSUALG_6, MSUALG_7, PARTFUN1, PBOOLE, PRALG_1, PRALG_2, PRALG_3,
      PRE_CIRC, PZFMISC1, RELAT_2, SETFAM_1, TARSKI, RELSET_1, XBOOLE_0,
      XBOOLE_1, ORDERS_1;
 schemes MSSUBFAM, MSUALG_1, MSUALG_8, FUNCT_2;

begin :: Preliminaries

reserve a, I for set,
        S for non empty non void ManySortedSign;

scheme MSSExD { I() -> non empty set, P[set,set] }:
 ex f being ManySortedSet of I() st for i being Element of I() holds P[i,f.i]
  provided
A1: for i being Element of I() ex j being set st P[i,j]
  proof
    defpred Z[set,set] means P[ $1,$2];
A2: for i being set st i in I() ex j being set st Z[i,j] by A1;
    consider f being ManySortedSet of I() such that
A3:   for i being set st i in I() holds Z[i,f.i] from MSSEx(A2);
    take f;
    let i be Element of I();
    thus thesis by A3;
  end;

definition let I be set,
               M be ManySortedSet of I;
 cluster locally-finite Element of Bool M;
existence
  proof
      [0]I c= M by PBOOLE:49;
    then [0]I is ManySortedSubset of M by MSUALG_2:def 1;
    then reconsider A = [0]I as Element of Bool M by CLOSURE2:def 1;
    take A;
    thus thesis;
  end;
end;

definition let I be set,
               M be non-empty ManySortedSet of I;
 cluster non-empty locally-finite ManySortedSubset of M;
existence
  proof
defpred P[set,set] means
 ex a being Element of M.$1 st $2 = {a};
A1: now
      let i be set such that i in I;
      consider a being Element of M.i;
      take j = {a};
      thus P[i,j];
    end;
    consider C being ManySortedSet of I such that
A2:   for i be set st i in I holds P[i,C.i] from MSSEx(A1);
      C is ManySortedSubset of M
    proof
      let i be set; assume
A3:     i in I;
      then consider a being Element of M.i such that
A4:     C.i = {a} by A2;
A5:   M.i is non empty by A3,PBOOLE:def 16;
      let q be set;
      assume q in C.i;
      then q = a by A4,TARSKI:def 1;
      hence q in M.i by A5;
    end;
    then reconsider C as ManySortedSubset of M;
    take C;
    thus C is non-empty
    proof
      let i be set;
      assume i in I;
      then consider a being Element of M.i such that
A6:     C.i = {a} by A2;
      thus C.i is non empty by A6;
    end;
    let i be set;
    assume i in I;
    then consider a being Element of M.i such that
A7:   C.i = {a} by A2;
    thus C.i is finite by A7;
  end;
end;

definition let S be non empty non void ManySortedSign,
               A be non-empty MSAlgebra over S,
               o be OperSymbol of S;
 cluster -> FinSequence-like Element of Args(o,A);
coherence
  proof
    let x be Element of Args(o,A);
      dom x = dom the_arity_of o by MSUALG_6:2;
    then consider n being Nat such that
A1:   dom x = Seg n by FINSEQ_1:def 2;
    take n;
    thus dom x = Seg n by A1;
  end;
end;

definition let S be non void non empty ManySortedSign,
               I be set,
               s be SortSymbol of S,
               F be MSAlgebra-Family of I, S;
 cluster -> Function-like Relation-like Element of (SORTS F).s;
coherence
  proof
    let x be Element of (SORTS F).s;
      x is Element of product Carrier(F,s) by PRALG_2:def 17;
    hence x is Function-like Relation-like;
  end;
end;

definition let S be non void non empty ManySortedSign,
               X be non-empty ManySortedSet of the carrier of S;
 cluster FreeGen X -> free non-empty;
coherence by MSAFREE:15,17;
end;

definition let S be non void non empty ManySortedSign,
               X be non-empty ManySortedSet of the carrier of S;
 cluster FreeMSA X -> free;
coherence by MSAFREE:18;
end;

definition let S be non empty non void ManySortedSign,
               A, B be non-empty MSAlgebra over S;
 cluster [:A,B:] -> non-empty;
coherence
  proof
    thus the Sorts of [:A,B:] is non-empty
    proof
        [:A,B:] = MSAlgebra (# [|the Sorts of A,the Sorts of B|],
             [[:the Charact of A,the Charact of B:]] #) by PRALG_2:def 15;
      hence thesis;
    end;
  end;
end;

theorem
  for X, Y being set, f being Function st a in dom f & f.a in [:X,Y:]
 holds f.a = [(pr1 f).a, (pr2 f).a]
  proof
    let X, Y be set,
        f be Function such that
A1:   a in dom f and
A2:   f.a in [:X,Y:];
A3: (pr1 f).a = (f.a)`1 by A1,DTCONSTR:def 2;
      (pr2 f).a = (f.a)`2 by A1,DTCONSTR:def 3;
    hence thesis by A2,A3,MCART_1:23;
  end;

theorem Th2:
for X being non empty set, Y being set, f being Function of X, {Y}
 holds rng f = {Y}
  proof
    let X be non empty set,
        Y be set,
        f be Function of X, {Y};
A1: dom f = X by FUNCT_2:def 1;
    thus rng f c= {Y} by RELSET_1:12;
    let q be set;
    assume q in {Y};
then A2: q = Y by TARSKI:def 1;
    consider x being set such that
A3:   x in X by XBOOLE_0:def 1;
      f.x = Y by A3,FUNCT_2:65;
    hence q in rng f by A1,A2,A3,FUNCT_1:def 5;
  end;

theorem Th3:
for A being non empty finite set ex f being Function of NAT, A st rng f = A
  proof
    let A be non empty finite set;
    consider p being FinSequence such that
A1:   rng p = A by FINSEQ_1:73;
      p is FinSequence of A
    proof
      thus rng p c= A by A1;
    end;
    then reconsider p as FinSequence of A;
defpred P[set,set] means
 ($1 in dom p implies $2 = p.$1) &
   (not $1 in dom p implies ex a being Element of A st $2 = a);
A2: for x being Element of NAT ex y being Element of A st P[x,y]
    proof
      let x be Element of NAT;
      per cases;
      suppose x in dom p;
        then reconsider px = p.x as Element of A by PARTFUN1:27;
        take px;
        thus x in dom p implies px = p.x;
        thus thesis;
      suppose
A3:       not x in dom p;
        consider a being Element of A;
        take a;
        thus x in dom p implies a = p.x by A3;
        thus thesis;
    end;
    consider f being Function of NAT, A such that
A4:   for x being Element of NAT holds P[x,f.x] from FuncExD(A2);
    take f;
    thus rng f c= A by RELSET_1:12;
    let q be set;
    assume q in A;
    then consider x being Element of NAT such that
A5:   x in dom p and
A6:   q = p.x by A1,PARTFUN1:26;
A7: f.x = p.x by A4,A5;
      dom f = NAT by FUNCT_2:def 1;
    hence q in rng f by A6,A7,FUNCT_1:def 5;
  end;

theorem Th4:
Class(nabla I) c= {I}
  proof
    let q be set;
    assume q in Class(nabla I);
    then consider x being set such that
A1:   x in I & q = Class(nabla I,x) by EQREL_1:def 5;
      Class(nabla I,x) = I by A1,EQREL_1:34;
    hence q in {I} by A1,TARSKI:def 1;
  end;

theorem Th5:
for I being non empty set holds Class(nabla I) = {I}
  proof
    let I be non empty set;
    thus Class(nabla I) c= {I} by Th4;
    let q be set;
    assume q in {I};
then A1: q = I by TARSKI:def 1;
    consider a being set such that
A2:   a in I by XBOOLE_0:def 1;
      Class(nabla I,a) = I by A2,EQREL_1:34;
    hence q in Class(nabla I) by A1,A2,EQREL_1:def 5;
  end;

theorem Th6:
ex A being ManySortedSet of I st {A} = I --> {a}
  proof
    deffunc F(set) = a;
    consider A being ManySortedSet of I such that
A1:   for i being set st i in I holds A.i = F(i) from MSSLambda;
    take A;
      now
      let i be set; assume
A2:     i in I;
      hence {A}.i = {A.i} by PZFMISC1:def 1
                .= {a} by A1,A2
                .= (I --> {a}).i by A2,FUNCOP_1:13;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem
  for A being ManySortedSet of I
 ex B being non-empty ManySortedSet of I st A c= B
  proof
    let A be ManySortedSet of I;
    consider a being set;
    deffunc F(set) = {a} \/ A.$1;
    consider f being ManySortedSet of I such that
A1:   for i be set st i in I holds f.i = F(i) from MSSLambda;
      f is non-empty
    proof
      let i be set;
      assume i in I;
      then f.i = {a} \/ A.i by A1;
      hence f.i is non empty;
    end;
    then reconsider f as non-empty ManySortedSet of I;
    take f;
    let i be set;
    assume i in I;
    then f.i = A.i \/ {a} by A1;
    hence A.i c= f.i by XBOOLE_1:7;
  end;

theorem
  for M being non-empty ManySortedSet of I
 for B being locally-finite ManySortedSubset of M
  ex C being non-empty locally-finite ManySortedSubset of M st B c= C
  proof
    let M be non-empty ManySortedSet of I,
        B be locally-finite ManySortedSubset of M;
defpred P[set,set] means
 ex a being Element of M.$1 st $2 = {a} \/ B.$1;
A1: now
      let i be set such that i in I;
      consider a being Element of M.i;
      take j = {a} \/ B.i;
      thus P[i,j];
    end;
    consider C being ManySortedSet of I such that
A2:   for i be set st i in I holds P[i,C.i] from MSSEx(A1);
A3: C is ManySortedSubset of M
    proof
      let i be set; assume
A4:     i in I;
      then consider a being Element of M.i such that
A5:     C.i = {a} \/ B.i by A2;
        B c= M by MSUALG_2:def 1;
then A6:   B.i c= M.i by A4,PBOOLE:def 5;
A7:   M.i is non empty by A4,PBOOLE:def 16;
      let q be set;
      assume q in C.i;
      then q in {a} or q in B.i by A5,XBOOLE_0:def 2;
      then q = a or q in M.i by A6,TARSKI:def 1;
      hence q in M.i by A7;
    end;
A8: C is non-empty
    proof
      let i be set;
      assume i in I;
      then consider a being Element of M.i such that
A9:     C.i = {a} \/ B.i by A2;
      thus C.i is non empty by A9;
    end;
      C is locally-finite
    proof
      let i be set; assume
A10:     i in I;
      then consider a being Element of M.i such that
A11:     C.i = {a} \/ B.i by A2;
      reconsider b = B.i as finite set by A10,PRE_CIRC:def 3;
        {a} \/ b is finite;
      hence C.i is finite by A11;
    end;
    then reconsider C as non-empty locally-finite ManySortedSubset of M
      by A3,A8;
    take C;
    let i be set;
    assume i in I;
    then consider a being Element of M.i such that
A12:   C.i = {a} \/ B.i by A2;
    thus B.i c= C.i by A12,XBOOLE_1:7;
  end;

theorem
  for A, B being ManySortedSet of I
 for F, G being ManySortedFunction of A, {B} holds F = G
  proof
    let A, B be ManySortedSet of I,
        F, G be ManySortedFunction of A, {B};
      now
      let i be set; assume
A1:     i in I;
      then A2:     F.i is Function of A.i, {B}.i & G.i is Function of A.i, {B}.
i
        by MSUALG_1:def 2;
        {B}.i = {B.i} by A1,PZFMISC1:def 1;
      hence F.i = G.i by A2,FUNCT_2:66;
    end;
    hence F = G by PBOOLE:3;
  end;

theorem Th10:
for A being non-empty ManySortedSet of I, B being ManySortedSet of I
 for F being ManySortedFunction of A, {B} holds F is "onto"
  proof
    let A be non-empty ManySortedSet of I,
        B be ManySortedSet of I,
        F be ManySortedFunction of A, {B};
    let i be set; assume
A1:   i in I;
then A2: A.i <> {} by PBOOLE:def 16;
A3: {B}.i = {B.i} by A1,PZFMISC1:def 1;
      F.i is Function of A.i, {B}.i by A1,MSUALG_1:def 2;
    hence rng(F.i) = {B}.i by A2,A3,Th2;
  end;

theorem Th11:
for A being ManySortedSet of I, B being non-empty ManySortedSet of I
 for F being ManySortedFunction of {A}, B holds F is "1-1"
  proof
    let A be ManySortedSet of I,
        B be non-empty ManySortedSet of I,
        F be ManySortedFunction of {A}, B;
      now
      let i be set; assume
A1:   i in I;
then A2:   {A}.i = {A.i} by PZFMISC1:def 1;
        F.i is Function of {A}.i, B.i by A1,MSUALG_1:def 2;
      hence F.i is one-to-one by A2,PARTFUN1:70;
    end;
    hence F is "1-1" by MSUALG_3:1;
  end;

theorem
  for X being non-empty ManySortedSet of the carrier of S
 holds Reverse X is "1-1"
  proof
    let X be non-empty ManySortedSet of the carrier of S;
      for i being set st i in the carrier of S
      holds (Reverse X).i is one-to-one
    proof
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
      set f = (Reverse X).s;
      let x1,x2 be set such that
A1:     x1 in dom ((Reverse X).i) and
A2:     x2 in dom ((Reverse X).i) and
A3:     ((Reverse X).i).x1 = ((Reverse X).i).x2;
A4:   f = Reverse(s,X) by MSAFREE:def 20;
then A5:   dom f = FreeGen(s,X) by FUNCT_2:def 1;
      then consider a1 being set such that
A6:     a1 in X.s and
A7:     x1 = root-tree [a1,s] by A1,MSAFREE:def 17;
      consider a2 being set such that
A8:     a2 in X.s and
A9:     x2 = root-tree [a2,s] by A2,A5,MSAFREE:def 17;
      set D = DTConMSA X;
A10:   [a1,s] in Terminals D by A6,MSAFREE:7;
      then reconsider t1 = [a1,s] as Symbol of D;
        t1`2 = s by MCART_1:7;
      then root-tree t1 in {root-tree tt where tt is Symbol of D :
                             tt in Terminals D & tt`2 = s} by A10;
      then root-tree t1 in FreeGen(s,X) by MSAFREE:14;
then A11:   f.x1 = [a1,s]`1 by A4,A7,MSAFREE:def 19
          .= a1 by MCART_1:7;
A12:   [a2,s] in Terminals D by A8,MSAFREE:7;
      then reconsider t2 = [a2,s] as Symbol of D;
        t2`2 = s by MCART_1:7;
      then root-tree t2 in {root-tree tt where tt is Symbol of D :
                             tt in Terminals D & tt`2 = s} by A12;
      then root-tree t2 in FreeGen(s,X) by MSAFREE:14;
      then f.x2 = [a2,s]`1 by A4,A9,MSAFREE:def 19
          .= a2 by MCART_1:7;
      hence x1 = x2 by A3,A7,A9,A11;
    end;
    hence Reverse X is "1-1" by MSUALG_3:1;
  end;

theorem
  for A being non-empty locally-finite ManySortedSet of I
 ex F being ManySortedFunction of I --> NAT, A st F is "onto"
  proof
    let A be non-empty locally-finite ManySortedSet of I;
defpred P[set,set] means
 ex f being Function of NAT, A.$1 st $2 = f & rng f = A.$1;
A1: for i being set st i in I ex j being set st P[i,j]
    proof
      let i be set;
      assume i in I;
      then A.i is non empty & A.i is finite by PBOOLE:def 16,PRE_CIRC:def 3;
        then consider f being Function of NAT, A.i such that
A2:     rng f = A.i by Th3;
      take j = f;
      thus P[i,j] by A2;
    end;
    consider F being ManySortedSet of I such that
A3:   for i being set st i in I holds P[i,F.i] from MSSEx(A1);
      F is ManySortedFunction of I --> NAT, A
    proof
      let i be set; assume
A4:     i in I;
      then consider f being Function of NAT, A.i such that
A5:     F.i = f and rng f = A.i by A3;
         (I --> NAT).i = NAT by A4,FUNCOP_1:13;
     hence F.i is Function of (I --> NAT).i, A.i by A5;
    end;
    then reconsider F as ManySortedFunction of I --> NAT, A;
    take F;
    let i be set;
    assume i in I;
    then consider f being Function of NAT, A.i such that
A6:   F.i = f & rng f = A.i by A3;
    thus rng (F.i) = A.i by A6;
  end;

theorem
  for S being non empty ManySortedSign
 for A being non-empty MSAlgebra over S
  for f, g being Element of product the Sorts of A st
 for i being set holds proj(the Sorts of A,i).f = proj(the Sorts of A,i).g
   holds f = g
  proof
    let S be non empty ManySortedSign,
        A be non-empty MSAlgebra over S,
        f, g be Element of product the Sorts of A such that
A1:  for i being set holds proj(the Sorts of A,i).f =
       proj(the Sorts of A,i).g;
    set X = the Sorts of A;
      now
      thus dom f = dom X by CARD_3:18
                .= dom g by CARD_3:18;
      let x be set such that x in dom f;
A2:   dom (proj(X,x)) = product X by PRALG_3:def 2;
      hence f.x = proj(X,x).f by PRALG_3:def 2
               .= proj(X,x).g by A1
               .= g.x by A2,PRALG_3:def 2;
    end;
    hence f = g by FUNCT_1:9;
  end;

theorem
  for I being non empty set
 for s being Element of S
  for A being MSAlgebra-Family of I,S
   for f, g being Element of product Carrier(A,s) st
    for a being Element of I
     holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g
  holds f = g
  proof
    let I be non empty set,
        s be Element of S,
        A be MSAlgebra-Family of I,S,
        f, g be Element of product Carrier(A,s) such that
A1:  for a being Element of I
       holds proj(Carrier(A,s),a).f = proj(Carrier(A,s),a).g;
      now
A2:   dom f = dom Carrier(A,s) by CARD_3:18;
      hence dom f = dom g by CARD_3:18;
      let x be set such that
A3:     x in dom f;
A4:   dom f = I by A2,PBOOLE:def 3;
A5:   dom (proj(Carrier(A,s),x)) = product Carrier(A,s) by PRALG_3:def 2;
      hence f.x = proj(Carrier(A,s),x).f by PRALG_3:def 2
               .= proj(Carrier(A,s),x).g by A1,A3,A4
               .= g.x by A5,PRALG_3:def 2;
    end;
    hence f = g by FUNCT_1:9;
  end;

theorem
  for A, B being non-empty MSAlgebra over S
 for C being non-empty MSSubAlgebra of A
  for h1 being ManySortedFunction of B, C st h1 is_homomorphism B, C
   for h2 being ManySortedFunction of B, A st h1 = h2
 holds h2 is_homomorphism B, A
  proof
    let A, B be non-empty MSAlgebra over S,
        C be non-empty MSSubAlgebra of A,
        h1 be ManySortedFunction of B, C such that
A1:   h1 is_homomorphism B, C;
    let h2 be ManySortedFunction of B, A such that
A2:   h1 = h2;
      the Sorts of C is ManySortedSubset of the Sorts of A
             by MSUALG_2:def 10;
    then id (the Sorts of C) is ManySortedFunction of C, A
             by EXTENS_1:9;
    then consider G be ManySortedFunction of C, A such that
A3:   G = id (the Sorts of C);
A4: G ** h1 = h1 by A3,MSUALG_3:4;
      G is_monomorphism C, A by A3,MSUALG_3:22;
    then G is_homomorphism C, A by MSUALG_3:def 11;
    hence h2 is_homomorphism B, A by A1,A2,A4,MSUALG_3:10;
  end;

theorem
  for A, B being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, B st F is_monomorphism A, B
  holds A, Image F are_isomorphic
  proof
    let A, B be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, B; assume
A1:   F is_monomorphism A, B;
    then F is_homomorphism A, B by MSUALG_3:def 11;
    then consider G being ManySortedFunction of A, Image F such that
A2:   G = F and
A3:   G is_epimorphism A, Image F by MSUALG_3:21;
    take G;
    thus G is_epimorphism A, Image F by A3;
    thus G is_homomorphism A, Image F by A3,MSUALG_3:def 10;
    thus G is "1-1" by A1,A2,MSUALG_3:def 11;
  end;

theorem Th18:
for A, B being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, B st F is "onto"
  for o being OperSymbol of S
   for x being Element of Args(o,B) holds
 ex y being Element of Args(o,A) st F # y = x
  proof
    let A, B be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, B such that
A1:   F is "onto";
    let o be OperSymbol of S,
        t be Element of Args(o,B);
    set D = len (the_arity_of o);
    reconsider E = (the Sorts of B)*(the_arity_of o)
      as non-empty ManySortedSet of dom (the_arity_of o);
A2: Args(o,B) = product E by PRALG_2:10;
A3: Seg D = dom the_arity_of o by FINSEQ_1:def 3
         .= dom ((the Sorts of B)*(the_arity_of o)) by PRALG_2:10
         .= dom t by A2,CARD_3:18;
defpred P[set,set] means
 ex y1 being Element of (the Sorts of A).((the_arity_of o)/.$1)
  st (F.((the_arity_of o)/.$1)).y1 = t.$1 & $2 = y1;
A4: for k being Nat st k in Seg D ex x being set st P[k,x]
    proof
      let k be Nat such that
A5:     k in Seg D;
      set s = (the_arity_of o)/.k;
A6:   rng (F.s) = (the Sorts of B).s by A1,MSUALG_3:def 3;
        k in dom the_arity_of o by A5,FINSEQ_1:def 3;
      then t.k in (the Sorts of B).s by MSUALG_6:2;
      then consider y1 being set such that
A7:     y1 in (the Sorts of A).s & F.s.y1 = t.k by A6,FUNCT_2:17;
      take y1;
      reconsider y2 = y1 as Element of (the Sorts of A).s by A7;
      take y2;
      thus thesis by A7;
    end;
    consider p being FinSequence such that
A8:   dom p = Seg D and
A9:   for k being Nat st k in Seg D holds P[k,p.k] from NonUniqSeqEx(A4);
A10: len p = len the_arity_of o by A8,FINSEQ_1:def 3;
      for k being Nat st k in dom p holds
      p.k in (the Sorts of A).((the_arity_of o)/.k)
    proof
      let k be Nat;
      assume k in dom p;
      then consider y1 being Element of (the Sorts of A).((the_arity_of o)/.k)
      such that
          F.((the_arity_of o)/.k).y1 = t.k and
A11:     p.k = y1 by A8,A9;
      thus p.k in (the Sorts of A).((the_arity_of o)/.k) by A11;
    end;
    then reconsider p as Element of Args(o,A) by A10,MSAFREE2:7;
    set fp = F # p;
    take p;
A12: dom fp = dom ((the Sorts of B)*(the_arity_of o)) by A2,CARD_3:18
          .= dom t by A2,CARD_3:18;
      for k being Nat st k in dom t holds fp.k = t.k
    proof
      let k be Nat; assume
A13:     k in dom t;
     then consider y1 being Element of (the Sorts of A).((the_arity_of o)/.k)
          such that
A14:     (F.((the_arity_of o)/.k)).y1 = t.k & p.k = y1 by A3,A9;
      thus fp.k = t.k by A3,A8,A13,A14,MSUALG_3:def 8;
    end;
    hence F # p = t by A12,FINSEQ_1:17;
  end;

theorem Th19:
for A being non-empty MSAlgebra over S, o being OperSymbol of S
 for x being Element of Args(o,A) holds
  Den(o,A).x in (the Sorts of A).(the_result_sort_of o)
  proof
    let A be non-empty MSAlgebra over S,
        o be OperSymbol of S,
        x be Element of Args(o,A);
      Den(o,A).x is Element of ((the Sorts of A) * the ResultSort of S).o
       by MSUALG_1:def 10;
    then Den(o,A).x is Element of (the Sorts of A).((the ResultSort of S).o)
       by FUNCT_2:21;
    then Den(o,A).x is Element of (the Sorts of A).(the_result_sort_of o)
      by MSUALG_1:def 7;
    hence thesis;
  end;

theorem Th20:
for A, B, C being non-empty MSAlgebra over S
 for F1 being ManySortedFunction of A, B
  for F2 being ManySortedFunction of A, C st
    F1 is_epimorphism A, B & F2 is_homomorphism A, C
 for G being ManySortedFunction of B, C st G ** F1 = F2
  holds G is_homomorphism B, C
  proof
    let A, B, C be non-empty MSAlgebra over S,
        F1 be ManySortedFunction of A, B,
        F2 be ManySortedFunction of A, C such that
A1:   F1 is_epimorphism A, B and
A2:   F2 is_homomorphism A, C;
    let G be ManySortedFunction of B, C such that
A3:   G ** F1 = F2;
    let o be OperSymbol of S such that Args(o,B) <> {};
    let x be Element of Args(o,B);
    set r = the_result_sort_of o;
      F1 is "onto" by A1,MSUALG_3:def 10;
    then consider y being Element of Args(o,A) such that
A4:   F1 # y = x by Th18;
      F1 is_homomorphism A, B by A1,MSUALG_3:def 10;
then A5: (F1.r).(Den(o,A).y) = Den(o,B).x by A4,MSUALG_3:def 9;
A6: Den(o,A).y is Element of (the Sorts of A).r by Th19;
A7: (F2.r).(Den(o,A).y) = Den(o,C).((G ** F1) # y) by A2,A3,MSUALG_3:def 9
                       .= Den(o,C).(G # x) by A4,MSUALG_3:8;
      (F2.r).(Den(o,A).y) = (G.r * F1.r).(Den(o,A).y) by A3,MSUALG_3:2
                       .= (G.r).(Den(o,B).x) by A5,A6,FUNCT_2:21;
    hence (G.(the_result_sort_of o)).(Den(o,B).x) = Den(o,C).(G#x) by A7;
  end;

reserve A, M for ManySortedSet of I,
        B, C for non-empty ManySortedSet of I;

definition let I be set;
           let A be ManySortedSet of I;
           let B, C be non-empty ManySortedSet of I;
           let F be ManySortedFunction of A, [|B,C|];
 func Mpr1 F -> ManySortedFunction of A, B means :Def1:
  for i being set st i in I holds it.i = pr1 (F.i);
existence
  proof
    deffunc G(set) = pr1 (F.$1);
    consider X be ManySortedSet of I such that
A1:  for i be set st i in I holds X.i = G(i) from MSSLambda;
      X is ManySortedFunction of A, B
    proof
      let i be set; assume
A2:     i in I;
then A3:   [|B,C|].i <> {} by PBOOLE:def 16;
A4:   X.i = pr1 (F.i) by A1,A2;
      reconsider Bi = B.i as non empty set by A2,PBOOLE:def 16;
      reconsider Xi = X.i as Function by A4;
A5:     F.i is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
        then dom (F.i) = A.i by A3,FUNCT_2:def 1;
then A6:     dom Xi = A.i by A4,DTCONSTR:def 2;
       rng Xi c= Bi
        proof
          let q be set such that
A7:         q in rng Xi;
          assume
A8:         not q in Bi;
          consider x be set such that
A9:         x in dom Xi and
A10:         Xi.x = q by A7,FUNCT_1:def 5;
A11:       x in dom (F.i) by A4,A9,DTCONSTR:def 2;
then A12:       Xi.x = (F.i.x)`1 by A4,DTCONSTR:def 2;
            rng (F.i) c= [|B,C|].i by A5,RELSET_1:12;
then A13:       rng (F.i) c= [:B.i,C.i:] by A2,PRALG_2:def 9;
            F.i.x in rng (F.i) by A11,FUNCT_1:def 5;
          hence contradiction by A8,A10,A12,A13,MCART_1:10;
        end;
      hence X.i is Function of A.i, B.i by A6,FUNCT_2:def 1,RELSET_1:11;
    end;
    then reconsider X as ManySortedFunction of A, B;
    take X;
    thus thesis by A1;
  end;
uniqueness
  proof
    let M, N be ManySortedFunction of A, B such that
A14:   (for i be set st i in I holds M.i = pr1 (F.i)) and
A15:   (for i be set st i in I holds N.i = pr1 (F.i));
      now
      let i be set; assume
A16:     i in I;
      hence M.i = pr1 (F.i) by A14
              .= N.i by A15,A16;
    end;
    hence M = N by PBOOLE:3;
  end;

 func Mpr2 F -> ManySortedFunction of A, C means :Def2:
  for i being set st i in I holds it.i = pr2 (F.i);
existence
  proof
    deffunc G(set) =pr2 (F.$1);
    consider X be ManySortedSet of I such that
A17:  for i be set st i in I holds X.i = G(i) from MSSLambda;
      X is ManySortedFunction of A, C
    proof
      let i be set; assume
A18:     i in I;
then A19:   [|B,C|].i <> {} by PBOOLE:def 16;
A20:   X.i = pr2 (F.i) by A17,A18;
      reconsider Ci = C.i as non empty set by A18,PBOOLE:def 16;
      reconsider Xi = X.i as Function by A20;
A21:     F.i is Function of A.i, [|B,C|].i by A18,MSUALG_1:def 2;
        then dom (F.i) = A.i by A19,FUNCT_2:def 1;
then A22:   dom Xi = A.i by A20,DTCONSTR:def 3;
     rng Xi c= Ci
        proof
          let q be set such that
A23:         q in rng Xi;
          assume
A24:         not q in Ci;
          consider x be set such that
A25:         x in dom Xi and
A26:         Xi.x = q by A23,FUNCT_1:def 5;
A27:       x in dom (F.i) by A20,A25,DTCONSTR:def 3;
then A28:       Xi.x = (F.i.x)`2 by A20,DTCONSTR:def 3;
            rng (F.i) c= [|B,C|].i by A21,RELSET_1:12;
then A29:       rng (F.i) c= [:B.i,C.i:] by A18,PRALG_2:def 9;
            F.i.x in rng (F.i) by A27,FUNCT_1:def 5;
          hence contradiction by A24,A26,A28,A29,MCART_1:10;
        end;
      hence X.i is Function of A.i, C.i by A22,FUNCT_2:def 1,RELSET_1:11;
    end;
    then reconsider X as ManySortedFunction of A, C;
    take X;
    thus thesis by A17;
  end;
uniqueness
  proof
    let M, N be ManySortedFunction of A, C such that
A30:   (for i be set st i in I holds M.i = pr2 (F.i)) and
A31:   (for i be set st i in I holds N.i = pr2 (F.i));
      now
      let i be set; assume
A32:     i in I;
      hence M.i = pr2 (F.i) by A30
              .= N.i by A31,A32;
    end;
    hence M = N by PBOOLE:3;
  end;
end;

theorem
  for F being ManySortedFunction of A, [| I-->{a} , I-->{a} |]
 holds Mpr1 F = Mpr2 F
  proof
    let F be ManySortedFunction of A, [| I-->{a} , I-->{a} |];
      now
      let i be set; assume
A1:     i in I;
then A2:     (Mpr1 F).i = pr1 (F.i) by Def1;
A3:     (Mpr2 F).i = pr2 (F.i) by A1,Def2;
A4:   dom (pr2 (F.i)) = dom (F.i) by DTCONSTR:def 3;
        now
        let y be set such that
A5:       y in dom (F.i);
A6:     (F.i) is Function of A.i, [| I-->{a} , I-->{a} |].i
                 by A1,MSUALG_1:def 2;
A7:     (F.i).y in rng (F.i) by A5,FUNCT_1:def 5;
          rng (F.i) c= [| I-->{a} , I-->{a} |].i by A6,RELSET_1:12;
then A8:     rng (F.i) c= [: (I-->{a}).i , (I-->{a}).i :] by A1,PRALG_2:def 9;
        then ((F.i).y)`1 in (I-->{a}).i by A7,MCART_1:10;
then A9:     ((F.i).y)`1 in {a} by A1,FUNCOP_1:13;
          ((F.i).y)`2 in (I-->{a}).i by A7,A8,MCART_1:10;
then A10:     ((F.i).y)`2 in {a} by A1,FUNCOP_1:13;
        thus (pr2 (F.i)).y = ((F.i).y)`2 by A5,DTCONSTR:def 3
                          .= a by A10,TARSKI:def 1
                          .= ((F.i).y)`1 by A9,TARSKI:def 1;
      end;
      hence (Mpr1 F).i = (Mpr2 F).i by A2,A3,A4,DTCONSTR:def 2;
    end;
    hence Mpr1 F = Mpr2 F by PBOOLE:3;
  end;

theorem
  for F being ManySortedFunction of A, [|B,C|] st F is "onto"
 holds Mpr1 F is "onto"
  proof
    let F be ManySortedFunction of A, [|B,C|] such that
A1:   F is "onto";
    let i be set; assume
A2:   i in I;
    then reconsider m = (Mpr1 F).i as Function of A.i, B.i by MSUALG_1:def 2;
      rng m = B.i
    proof
        A is_transformable_to B
      proof
        let j be set;
        assume j in I;
        hence B.j = {} implies A.j = {} by PBOOLE:def 16;
      end;
      then rngs Mpr1 F c= B by MSSUBFAM:17;
      then (rngs Mpr1 F).i c= B.i by A2,PBOOLE:def 5;
      hence rng m c= B.i by A2,MSSUBFAM:13;
      let a be set such that
A3:     a in B.i;
A4:   (F.i) is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
A5:   rng (F.i) = [|B,C|].i by A1,A2,MSUALG_3:def 3;
A6:   [|B,C|].i <> {} by A2,PBOOLE:def 16;
      then consider z be set such that
A7:     z in [|B,C|].i by XBOOLE_0:def 1;
A8:   z in [:B.i,C.i:] by A2,A7,PRALG_2:def 9;
      set p = [a,z`2];
A9:   p`1 in B.i by A3,MCART_1:7;
        p`2 = z`2 by MCART_1:7;
      then p`2 in C.i by A8,MCART_1:10;
      then p in [:B.i,C.i:] by A9,MCART_1:11;
      then p in [|B,C|].i by A2,PRALG_2:def 9;
      then consider b be set such that
A10:     b in A.i and
A11:     (F.i).b = p by A4,A5,FUNCT_2:17;
A12:   dom (F.i) = A.i by A4,A6,FUNCT_2:def 1;
        B.i <> {} by A2,PBOOLE:def 16;
then A13:   dom m = A.i by FUNCT_2:def 1;
        m.b = (pr1 (F.i)).b by A2,Def1
         .= p`1 by A10,A11,A12,DTCONSTR:def 2
         .= a by MCART_1:7;
      hence a in rng m by A10,A13,FUNCT_1:def 5;
    end;
    hence thesis;
  end;

theorem
  for F being ManySortedFunction of A, [|B,C|] st F is "onto"
 holds Mpr2 F is "onto"
  proof
    let F be ManySortedFunction of A, [|B,C|] such that
A1:   F is "onto";
    let i be set; assume
A2:   i in I;
    then reconsider m = (Mpr2 F).i as Function of A.i, C.i by MSUALG_1:def 2;
      rng m = C.i
    proof
        A is_transformable_to C
      proof
        let j be set;
        assume j in I;
        hence C.j = {} implies A.j = {} by PBOOLE:def 16;
      end;
      then rngs Mpr2 F c= C by MSSUBFAM:17;
      then (rngs Mpr2 F).i c= C.i by A2,PBOOLE:def 5;
      hence rng m c= C.i by A2,MSSUBFAM:13;
      let a be set such that
A3:     a in C.i;
A4:   (F.i) is Function of A.i, [|B,C|].i by A2,MSUALG_1:def 2;
A5:   rng (F.i) = [|B,C|].i by A1,A2,MSUALG_3:def 3;
A6:   [|B,C|].i <> {} by A2,PBOOLE:def 16;
      then consider z be set such that
A7:     z in [|B,C|].i by XBOOLE_0:def 1;
A8:   z in [:B.i,C.i:] by A2,A7,PRALG_2:def 9;
      set p = [z`1,a];
A9:   p`2 in C.i by A3,MCART_1:7;
        p`1 = z`1 by MCART_1:7;
      then p`1 in B.i by A8,MCART_1:10;
      then p in [:B.i,C.i:] by A9,MCART_1:11;
      then p in [|B,C|].i by A2,PRALG_2:def 9;
      then consider b be set such that
A10:     b in A.i and
A11:     (F.i).b = p by A4,A5,FUNCT_2:17;
A12:   dom (F.i) = A.i by A4,A6,FUNCT_2:def 1;
        C.i <> {} by A2,PBOOLE:def 16;
then A13:   dom m = A.i by FUNCT_2:def 1;
        m.b = (pr2 (F.i)).b by A2,Def2
         .= p`2 by A10,A11,A12,DTCONSTR:def 3
         .= a by MCART_1:7;
      hence a in rng m by A10,A13,FUNCT_1:def 5;
    end;
    hence thesis;
  end;

theorem
  for F being ManySortedFunction of A, [|B,C|] st M in doms F holds
 for i be set st i in I holds (F..M).i = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i]
  proof
    let F be ManySortedFunction of A, [|B,C|] such that
A1:   M in doms F;
    let i be set; assume
A2:   i in I;
then A3: (Mpr1 F).i = pr1 (F.i) by Def1;
A4: (Mpr2 F).i = pr2 (F.i) by A2,Def2;
A5: dom F = I by PBOOLE:def 3;
      A is_transformable_to [|B,C|]
    proof
      let i be set;
      assume i in I;
      hence [|B,C|].i = {} implies A.i = {} by PBOOLE:def 16;
    end;
    then M in A by A1,MSSUBFAM:17;
    then F..M in [|B,C|] by CLOSURE1:3;
    then (F..M).i in [|B,C|].i by A2,PBOOLE:def 4;
    then (F..M).i in [:B.i,C.i:] by A2,PRALG_2:def 9;
then A6: (F.i).(M.i) in [:B.i,C.i:] by A2,A5,PRALG_1:def 18;
    set z = (F.i).(M.i);
      M.i in (doms F).i by A1,A2,PBOOLE:def 4;
then A7: M.i in dom (F.i) by A2,MSSUBFAM:14;
      dom (Mpr1 F) = I by PBOOLE:def 3;
then A8: ((Mpr1 F)..M).i = (pr1 (F.i)).(M.i) by A2,A3,PRALG_1:def 18
                   .= z`1 by A7,DTCONSTR:def 2;
      dom (Mpr2 F) = I by PBOOLE:def 3;
    then ((Mpr2 F)..M).i = (pr2 (F.i)).(M.i) by A2,A4,PRALG_1:def 18
                   .= z`2 by A7,DTCONSTR:def 3;
    then z = [((Mpr1 F)..M).i, ((Mpr2 F)..M).i] by A6,A8,MCART_1:23;
    hence thesis by A2,A5,PRALG_1:def 18;
  end;


begin :: On the Trivial Many Sorted Algebras

definition let S be non empty ManySortedSign;
 cluster the Sorts of Trivial_Algebra S -> locally-finite non-empty;
coherence
  proof
    consider A being ManySortedSet of the carrier of S such that
A1:   {A} = (the carrier of S) --> {0} by Th6;
    thus thesis by A1,MSAFREE2:def 12;
  end;
end;

definition let S be non empty ManySortedSign;
 cluster Trivial_Algebra S -> locally-finite non-empty;
coherence
  proof
    thus the Sorts of Trivial_Algebra S is locally-finite;
    let i be set such that
A1:   i in the carrier of S;
      the Sorts of Trivial_Algebra S = (the carrier of S) --> {0}
      by MSAFREE2:def 12;
    hence (the Sorts of Trivial_Algebra S).i is non empty by A1,FUNCOP_1:13;
  end;
end;

theorem Th25:
for A being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, Trivial_Algebra S
  for o being OperSymbol of S
   for x being Element of Args(o,A) holds
 (F.the_result_sort_of o).(Den(o,A).x) = 0 &
  Den(o,Trivial_Algebra S).(F#x) = 0
  proof
    let A be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, Trivial_Algebra S;
    let o be OperSymbol of S;
    let x be Element of Args(o,A);
    set I = the carrier of S,
        SA = the Sorts of A,
        T = Trivial_Algebra S,
        ST = the Sorts of T;
    consider XX being ManySortedSet of I such that
A1:   {XX} = I --> {0} by Th6;
A2: ST = {XX} by A1,MSAFREE2:def 12;
    set r = the_result_sort_of o;
    consider i being set such that
A3:   i in I and
A4:   Result(o,T) = ST.i by MSUALG_1:2;
A5: ST.i = {0} by A1,A2,A3,FUNCOP_1:13;
      Den(o,A).x in Result(o,A);
    then Den(o,A).x in ((the Sorts of A) * the ResultSort of S).o
       by MSUALG_1:def 10;
    then Den(o,A).x in (the Sorts of A).((the ResultSort of S).o)
       by FUNCT_2:21;
    then reconsider d = Den(o,A).x as Element of SA.r by MSUALG_1:def 7;
A6: ST.r = {0} by A1,A2,FUNCOP_1:13;
    thus (F.r).(Den(o,A).x) = (F.r).d
                           .= 0 by A6,TARSKI:def 1;
    thus Den(o,T).(F#x) = 0 by A4,A5,TARSKI:def 1;
  end;

theorem Th26:
for A being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, Trivial_Algebra S holds
  F is_epimorphism A, Trivial_Algebra S
  proof
    let A be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, Trivial_Algebra S;
    set I = the carrier of S;
    consider XX being ManySortedSet of I such that
A1:   {XX} = I --> {0} by Th6;
A2: the Sorts of Trivial_Algebra S = {XX} by A1,MSAFREE2:def 12;
    thus F is_homomorphism A, Trivial_Algebra S
    proof
      let o be OperSymbol of S such that Args(o,A) <> {};
      let x be Element of Args(o,A);
      thus (F.the_result_sort_of o).(Den(o,A).x) = 0 by Th25
        .= Den(o,Trivial_Algebra S).(F#x) by Th25;
    end;
    thus F is "onto" by A2,Th10;
  end;

theorem
  for A being MSAlgebra over S st
 ex X being ManySortedSet of the carrier of S st the Sorts of A = {X}
  holds A, Trivial_Algebra S are_isomorphic
  proof
    let A be MSAlgebra over S such that
A1:   ex X being ManySortedSet of the carrier of S st the Sorts of A = {X};
    set I = the carrier of S,
        SB = the Sorts of A,
        ST = the Sorts of Trivial_Algebra S;
    consider X being ManySortedSet of I such that
A2:   the Sorts of A = {X} by A1;
    consider F being ManySortedFunction of SB, ST;
    take F;
    reconsider F1 = F as ManySortedFunction of {X}, ST by A2;
      A is non-empty by A2,MSUALG_1:def 8;
    hence F is_epimorphism A, Trivial_Algebra S by Th26;
    hence F is_homomorphism A, Trivial_Algebra S by MSUALG_3:def 10;
      F1 is "1-1" by Th11;
    hence F is "1-1";
  end;


begin :: On the Many Sorted Congruences

theorem
  for A being non-empty MSAlgebra over S
 for C being MSCongruence of A holds
  C is ManySortedSubset of [|the Sorts of A, the Sorts of A|]
  proof
    let A be non-empty MSAlgebra over S,
        C be MSCongruence of A;
    let i be set such that
A1:   i in the carrier of S;
    set SF = the Sorts of A;
      C.i is Relation of SF.i, SF.i by A1,MSUALG_4:def 2;
    then C.i c= [:SF.i, SF.i:];
    hence C.i c= [|SF,SF|].i by A1,PRALG_2:def 9;
  end;

theorem
  for A being non-empty MSAlgebra over S
 for R being Subset of CongrLatt A
  for F being SubsetFamily of [|the Sorts of A, the Sorts of A|]
   st R = F holds meet |:F:| is MSCongruence of A
  proof
    let A be non-empty MSAlgebra over S,
        R be Subset of CongrLatt A,
        F be SubsetFamily of [|the Sorts of A, the Sorts of A|]
        such that
A1:   R = F;
    set R0 = meet |:F:|,
        SF = the Sorts of A,
        I = the carrier of S;
    per cases;
    suppose F is non empty;
    then reconsider F1 = F as non empty SubsetFamily of [|SF,SF|];
      F1 c= the carrier of EqRelLatt SF
    proof
      let q be set;
      assume q in F1;
      then q is MSCongruence of A by A1,MSUALG_5:def 6;
      hence q in the carrier of EqRelLatt SF by MSUALG_5:def 5;
    end;
then A2: R0 is MSEquivalence_Relation-like ManySortedRelation of SF
       by MSUALG_7:9;
    then reconsider R0 as ManySortedRelation of A;
      R0 is MSEquivalence-like
    proof
      let i be set,
          R be Relation of SF.i;
      assume i in I & R0.i = R;
      hence R is Equivalence_Relation of SF.i by A2,MSUALG_4:def 3;
    end;
    then reconsider R0 as MSEquivalence-like ManySortedRelation of A;
      now
      let o be OperSymbol of S;
      let a,b be Element of Args(o,A) such that
A3:     for n being Nat st n in dom a holds [a.n,b.n] in
 R0.((the_arity_of o)/.n);
      set r = the_result_sort_of o;
      consider Q being Subset-Family of ([|SF,SF|].r) such that
A4:     Q = |:F1:|.r and
A5:     R0.r = Intersect Q by MSSUBFAM:def 2;
A6:   Q = { s.r where s is Element of Bool [|SF,SF|] : s in F1 }
        by A4,CLOSURE2:15;
        now
        let Y be set;
        assume Y in Q;
        then consider s being Element of Bool [|SF,SF|] such that
A7:       Y = s.r and
A8:       s in F1 by A6;
        reconsider s as MSCongruence of A by A1,A8,MSUALG_5:def 6;
          now
          let n be Nat such that
A9:         n in dom a;
          set t = (the_arity_of o)/.n;
          consider G being Subset-Family of ([|SF,SF|].t) such that
A10:         G = |:F1:|.t and
A11:         R0.t = Intersect G by MSSUBFAM:def 2;
            [a.n,b.n] in Intersect G by A3,A9,A11;
then A12:       [a.n,b.n] in meet G by A10,CANTOR_1:def 3;
            G = { j.t where j is Element of Bool [|SF,SF|] : j in F1 }
                 by A10,CLOSURE2:15;
          then s.t in G by A8;
          hence [a.n,b.n] in s.t by A12,SETFAM_1:def 1;
        end;
        hence [Den(o,A).a,Den(o,A).b] in Y by A7,MSUALG_4:def 6;
      end;
      then [Den(o,A).a,Den(o,A).b] in meet Q by A4,SETFAM_1:def 1;
      hence [Den(o,A).a,Den(o,A).b] in R0.(the_result_sort_of o)
         by A4,A5,CANTOR_1:def 3;
    end;
    hence thesis by MSUALG_4:def 6;
    suppose F is empty;
    then |:F:| = [0]I by CLOSURE2:def 4;
    then meet |:F:| = [|the Sorts of A, the Sorts of A|] by MSSUBFAM:41;
    hence thesis by MSUALG_5:20;
  end;

theorem
  for A being non-empty MSAlgebra over S
 for C being MSCongruence of A st C = [|the Sorts of A, the Sorts of A|]
  holds the Sorts of QuotMSAlg (A,C) = {the Sorts of A}
  proof
    let A be non-empty MSAlgebra over S,
        C be MSCongruence of A such that
A1:   C = [|the Sorts of A, the Sorts of A|];
      now
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as Element of S;
A2:   QuotMSAlg (A,C) = MSAlgebra (# Class C, QuotCharact C #)
        by MSUALG_4:def 16;
A3:   C.s = [:(the Sorts of A).s, (the Sorts of A).s:] by A1,PRALG_2:def 9
         .= nabla (the Sorts of A).s by EQREL_1:def 1;
      thus (the Sorts of QuotMSAlg (A,C)).i
          = Class (C.s) by A2,MSUALG_4:def 8
         .= {(the Sorts of A).s} by A3,Th5
         .= {the Sorts of A}.i by PZFMISC1:def 1;
    end;
    hence thesis by PBOOLE:3;
  end;

theorem Th31:
for A, B being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, B st F is_homomorphism A, B
  holds MSHomQuot F ** MSNat_Hom(A,MSCng F) = F
  proof
    let A, B be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, B such that
A1:   F is_homomorphism A, B;
      now
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
        QuotMSAlg (A,MSCng F) = MSAlgebra(# Class MSCng F, QuotCharact MSCng F
#)
          by MSUALG_4:def 16;
      then reconsider h = MSHomQuot(F,s) as Function of (Class MSCng F).s,
                                            (the Sorts of B).s;
      reconsider f = h * MSNat_Hom(A,MSCng F,s) as Function of
        (the Sorts of A).s, (the Sorts of B).s;
A2:   for c being Element of (the Sorts of A).s holds f.c = F.s.c
      proof
        let c be Element of (the Sorts of A).s;
        thus f.c
            = h.((MSNat_Hom(A,MSCng F,s)).c) by FUNCT_2:21
           .= h.(Class((MSCng F).s,c)) by MSUALG_4:def 17
           .= h.(Class(MSCng(F,s),c)) by A1,MSUALG_4:def 20
           .= F.s.c by A1,MSUALG_4:def 21;
      end;
      thus (MSHomQuot F ** MSNat_Hom(A,MSCng F)).i
         = ((MSHomQuot F).s) * ((MSNat_Hom(A,MSCng F)).s) by MSUALG_3:2
        .= MSHomQuot(F,s) * ((MSNat_Hom(A,MSCng F)).s) by MSUALG_4:def 22
        .= MSHomQuot(F,s) * MSNat_Hom(A,MSCng F,s) by MSUALG_4:def 18
        .= F.i by A2,FUNCT_2:113;
    end;
    hence MSHomQuot F ** MSNat_Hom(A,MSCng F) = F by PBOOLE:3;
  end;

theorem Th32:
for A being non-empty MSAlgebra over S
 for C being MSCongruence of A
  for s being SortSymbol of S
   for a being Element of (the Sorts of QuotMSAlg (A,C)).s
 ex x being Element of (the Sorts of A).s st a = Class(C,x)
  proof
    let A be non-empty MSAlgebra over S,
        C be MSCongruence of A,
        s be SortSymbol of S,
        a be Element of (the Sorts of QuotMSAlg (A,C)).s;
      QuotMSAlg (A,C) = MSAlgebra (#Class C, QuotCharact C#)
      by MSUALG_4:def 16;
    then a in (Class C).s;
    then a in Class (C.s) by MSUALG_4:def 8;
    then consider t being set such that
A1:   t in (the Sorts of A).s and
A2:   a = Class(C.s,t) by EQREL_1:def 5;
    reconsider t as Element of (the Sorts of A).s by A1;
    take t;
    thus thesis by A2,MSUALG_4:def 7;
  end;

theorem
  for A being MSAlgebra over S
 for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2
  for i being Element of S
   for x, y being Element of (the Sorts of A).i st [x,y] in C1.i
 holds Class (C1,x) c= Class (C2,y) &
  (A is non-empty implies Class (C1,y) c= Class (C2,x))
  proof
    let A be MSAlgebra over S,
        C1, C2 be MSEquivalence-like ManySortedRelation of A such that
A1:   C1 c= C2;
    let i be Element of S,
        x, y be Element of (the Sorts of A).i such that
A2:   [x,y] in C1.i;
A3: C1.i c= C2.i by A1,PBOOLE:def 5;
    field(C1.i) = (the Sorts of A).i by ORDERS_1:97;
    then
A4: C1.i is_transitive_in (the Sorts of A).i by RELAT_2:def 16;
    thus Class (C1,x) c= Class (C2,y)
    proof
      let q be set; assume
A5:     q in Class (C1,x);
      then q in Class(C1.i,x) by MSUALG_4:def 7;
      then [q,x] in C1.i by EQREL_1:27;
      then [q,y] in C1.i by A2,A4,A5,RELAT_2:def 8;
      then q in Class(C2.i,y) by A3,EQREL_1:27;
      hence q in Class (C2,y) by MSUALG_4:def 7;
    end;
    assume A is non-empty;
    then reconsider B = A as non-empty MSAlgebra over S;
    let q be set such that
A6:   q in Class (C1,y);
    field(C1.i) = (the Sorts of A).i by ORDERS_1:97;
    then C1.i is_symmetric_in (the Sorts of B).i by RELAT_2:def 11;
then A7: [y,x] in C1.i by A2,RELAT_2:def 3;
      q in Class(C1.i,y) by A6,MSUALG_4:def 7;
    then [q,y] in C1.i by EQREL_1:27;
    then [q,x] in C1.i by A4,A6,A7,RELAT_2:def 8;
    then q in Class(C2.i,x) by A3,EQREL_1:27;
    hence q in Class (C2,x) by MSUALG_4:def 7;
  end;

theorem
  for A being non-empty MSAlgebra over S, C being MSCongruence of A
 for s being SortSymbol of S, x, y being Element of (the Sorts of A).s holds
  (MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y iff [x,y] in C.s
  proof
    let A be non-empty MSAlgebra over S,
        C be MSCongruence of A,
        s be SortSymbol of S,
        x, y be Element of (the Sorts of A).s;
    set f = (MSNat_Hom(A,C)).s,
        g = MSNat_Hom(A,C,s);
A1: f = g by MSUALG_4:def 18;
    hereby
      assume
A2:     (MSNat_Hom(A,C)).s.x = (MSNat_Hom(A,C)).s.y;
        Class(C.s,x) = g.x by MSUALG_4:def 17
                  .= Class(C.s,y) by A1,A2,MSUALG_4:def 17;
      hence [x,y] in C.s by EQREL_1:44;
    end;
    assume
A3:   [x,y] in C.s;
    thus (MSNat_Hom(A,C)).s.x = Class(C.s,x) by A1,MSUALG_4:def 17
                             .= Class(C.s,y) by A3,EQREL_1:44
                             .= (MSNat_Hom(A,C)).s.y by A1,MSUALG_4:def 17;
  end;

Lm1:
  now
    let S be non empty non void ManySortedSign,
        A be non-empty MSAlgebra over S,
        C1, C2 be MSCongruence of A;
    let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A1: for i being Element of S
     for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
      for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
       G.i.x = Class(C2, xx);
    thus G is "onto"
    proof
      set sL = the Sorts of QuotMSAlg (A,C1),
          sP = the Sorts of QuotMSAlg (A,C2);
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
        rng(G.s) c= sP.s by RELSET_1:12;
      hence rng(G.i) c= sP.i;
      let q be set such that
A2:     q in sP.i;
        QuotMSAlg (A,C2) = MSAlgebra (#Class C2, QuotCharact C2#)
        by MSUALG_4:def 16;
      then q in Class(C2.s) by A2,MSUALG_4:def 8;
      then consider a being set such that
A3:     a in (the Sorts of A).s and
A4:     q = Class(C2.s,a) by EQREL_1:def 5;
      reconsider a as Element of (the Sorts of A).s by A3;
A5:   dom (G.s) = sL.s by FUNCT_2:def 1;
A6:   QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
        by MSUALG_4:def 16;
        Class(C1.s,a) in Class (C1.s) by EQREL_1:def 5;
      then Class(C1,a) in Class (C1.s) by MSUALG_4:def 7;
      then reconsider x = Class(C1,a) as Element of sL.s by A6,MSUALG_4:def 8;
        G.s.x = Class(C2,a) by A1
           .= Class(C2.s,a) by MSUALG_4:def 7;
      hence q in rng(G.i) by A4,A5,FUNCT_1:def 5;
    end;
  end;

theorem Th35:
for A being non-empty MSAlgebra over S
 for C1, C2 being MSCongruence of A
  for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) st
   for i being Element of S
    for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
     for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
      G.i.x = Class(C2,xx) holds
 G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2)
  proof
    let A be non-empty MSAlgebra over S,
        C1, C2 be MSCongruence of A;
    let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A1:  for i being Element of S
      for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
       for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
        G.i.x = Class(C2,xx);
    set sL = the Sorts of QuotMSAlg (A,C1);
      now
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
A2:   for c being Element of (the Sorts of A).s holds
        ((G.s) * (MSNat_Hom(A,C1).s)).c = MSNat_Hom(A,C2).s.c
      proof
        let c be Element of (the Sorts of A).s;
A3:     QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
          by MSUALG_4:def 16;
          Class(C1.s,c) in Class (C1.s) by EQREL_1:def 5;
        then Class(C1,c) in Class (C1.s) by MSUALG_4:def 7;
then A4:     Class(C1,c) is Element of sL.s by A3,MSUALG_4:def 8;
        thus ((G.s) * (MSNat_Hom(A,C1).s)).c
           = (G.s).(MSNat_Hom(A,C1).s.c) by FUNCT_2:21
          .= (G.s).(MSNat_Hom(A,C1,s).c) by MSUALG_4:def 18
          .= (G.s).Class(C1.s,c) by MSUALG_4:def 17
          .= (G.s).Class(C1,c) by MSUALG_4:def 7
          .= Class(C2,c) by A1,A4
          .= Class(C2.s,c) by MSUALG_4:def 7
          .= MSNat_Hom(A,C2,s).c by MSUALG_4:def 17
          .= MSNat_Hom(A,C2).s.c by MSUALG_4:def 18;
      end;
      thus (G ** MSNat_Hom(A,C1)).i
         = (G.s) * (MSNat_Hom(A,C1).s) by MSUALG_3:2
        .= MSNat_Hom(A,C2).i by A2,FUNCT_2:113;
    end;
    hence G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2) by PBOOLE:3;
  end;

theorem Th36:
for A being non-empty MSAlgebra over S
 for C1, C2 being MSCongruence of A
  for G being ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) st
   for i being Element of S
    for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
     for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
      G.i.x = Class(C2,xx) holds
  G is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2)
  proof
    let A be non-empty MSAlgebra over S,
        C1, C2 be MSCongruence of A;
    let G be ManySortedFunction of QuotMSAlg (A,C1), QuotMSAlg (A,C2) such that
A1:  for i being Element of S
      for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
       for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
        G.i.x = Class(C2,xx);
A2: MSNat_Hom(A,C1) is_epimorphism A, QuotMSAlg (A,C1) by MSUALG_4:3;
      MSNat_Hom(A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3;
then A3: MSNat_Hom(A,C2) is_homomorphism A, QuotMSAlg (A,C2) by MSUALG_3:def 10
;
      G ** MSNat_Hom(A,C1) = MSNat_Hom(A,C2) by A1,Th35;
    hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A2,A3,Th20;
    thus G is "onto" by A1,Lm1;
  end;

theorem
  for A, B being non-empty MSAlgebra over S
 for F being ManySortedFunction of A, B st F is_homomorphism A, B
  for C1 being MSCongruence of A st C1 c= MSCng F
 ex H being ManySortedFunction of QuotMSAlg (A,C1), B st
  H is_homomorphism QuotMSAlg (A,C1), B & F = H ** MSNat_Hom(A,C1)
  proof
    let A, B be non-empty MSAlgebra over S,
        F be ManySortedFunction of A, B such that
A1:   F is_homomorphism A, B;
    let C1 be MSCongruence of A such that
A2:   C1 c= MSCng F;
    set G = MSNat_Hom(A,C1),
        I = the carrier of S,
        sQ = the Sorts of QuotMSAlg (A,C1),
        sF = the Sorts of QuotMSAlg (A,MSCng F);
defpred P[set,set,set] means
 ex s being Element of I, xx being Element of (the Sorts of A).s st
  $3 = s & $2 = Class(C1,xx) & $1 = Class(MSCng F,xx);
A3: for i being set st i in I holds
     for x being set st x in sQ.i ex y being set st y in sF.i & P[y,x,i]
    proof
      let i be set;
      assume i in I;
      then reconsider s = i as Element of I;
      let x be set;
      assume x in sQ.i;
      then consider x1 being Element of (the Sorts of A).s such that
A4:     x = Class(C1,x1) by Th32;
      take y = Class(MSCng F,x1);
        y = Class((MSCng F).s,x1) by MSUALG_4:def 7;
then A5:   y in Class ((MSCng F).s) by EQREL_1:def 5;
        QuotMSAlg (A,MSCng F) = MSAlgebra (#Class MSCng F, QuotCharact MSCng F
#)
        by MSUALG_4:def 16;
      hence y in sF.i by A5,MSUALG_4:def 8;
      thus P[y,x,i] by A4;
    end;
    consider C12 being ManySortedFunction of sQ, sF such that
A6:  for i being set st i in I holds
      ex f being Function of sQ.i, sF.i st f = C12.i &
       for x being set st x in sQ.i holds P[f.x,x,i] from MSFExFunc(A3);
A7: for i being Element of S
     for x being Element of (the Sorts of QuotMSAlg (A,C1)).i
      for xx being Element of (the Sorts of A).i st x = Class(C1,xx) holds
       C12.i.x = Class(MSCng F,xx)
     proof
       let i be Element of S,
           x be Element of (the Sorts of QuotMSAlg (A,C1)).i,
           xx be Element of (the Sorts of A).i such that
A8:      x = Class(C1,xx);
       consider f being Function of sQ.i, sF.i such that
A9:      f = C12.i and
A10:      for x being set st x in sQ.i holds P[f.x,x,i] by A6;
       consider s being Element of I,
                x1 being Element of (the Sorts of A).s such that
A11:      i = s and
A12:      x = Class(C1,x1) and
A13:      f.x = Class(MSCng F,x1) by A10;
A14:    C1.s c= (MSCng F).s by A2,PBOOLE:def 5;
         Class(C1.s,x1) = Class(C1,x1) by MSUALG_4:def 7
                     .= Class(C1.s,xx) by A8,A11,A12,MSUALG_4:def 7;
         then xx in Class(C1.s,x1) by EQREL_1:31;
       then [xx,x1] in C1.s by EQREL_1:27;
then A15:    xx in Class((MSCng F).s,x1) by A14,EQREL_1:27;
       thus C12.i.x = Class((MSCng F).s, x1) by A9,A13,MSUALG_4:def 7
                   .= Class((MSCng F).i, xx) by A11,A15,EQREL_1:31
                   .= Class(MSCng F, xx) by MSUALG_4:def 7;
    end;
    then C12 is_epimorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F) by Th36;
then A16: C12 is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,MSCng F)
       by MSUALG_3:def 10;
    reconsider H = MSHomQuot F**C12
      as ManySortedFunction of QuotMSAlg (A,C1), B;
    take H;
      MSHomQuot F is_monomorphism QuotMSAlg (A,MSCng F), B by A1,MSUALG_4:4;
    then MSHomQuot F is_homomorphism QuotMSAlg (A,MSCng F), B by MSUALG_3:def
11;
    hence H is_homomorphism QuotMSAlg (A,C1), B by A16,MSUALG_3:10;
A17: now
      let i be set;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
A18:   for x being Element of (the Sorts of A).s holds
        (C12.s * G.s).x = (MSNat_Hom(A,MSCng F)).s.x
      proof
        let x be Element of (the Sorts of A).s;
          Class(C1.s,x) in Class (C1.s) by EQREL_1:def 5;
        then Class(C1,x) in Class (C1.s) by MSUALG_4:def 7;
then A19:     Class(C1,x) in (Class C1).s by MSUALG_4:def 8;
A20:     QuotMSAlg (A,C1) = MSAlgebra (#Class C1, QuotCharact C1#)
          by MSUALG_4:def 16;
        thus (C12.s * G.s).x
          = C12.s.(G.s.x) by FUNCT_2:21
         .= C12.s.(MSNat_Hom(A,C1,s).x) by MSUALG_4:def 18
         .= C12.s.(Class(C1.s,x)) by MSUALG_4:def 17
         .= C12.s.(Class(C1,x)) by MSUALG_4:def 7
         .= Class(MSCng F,x) by A7,A19,A20
         .= Class((MSCng F).s,x) by MSUALG_4:def 7
         .= MSNat_Hom(A,MSCng F,s).x by MSUALG_4:def 17
         .= (MSNat_Hom(A,MSCng F)).s.x by MSUALG_4:def 18;
      end;
      thus (C12 ** G).i = C12.s * G.s by MSUALG_3:2
                       .= (MSNat_Hom(A,MSCng F)).i by A18,FUNCT_2:113;
    end;
    thus F = MSHomQuot F ** MSNat_Hom(A,MSCng F) by A1,Th31
          .= MSHomQuot F ** (C12 ** G) by A17,PBOOLE:3
          .= H ** MSNat_Hom(A,C1) by AUTALG_1:13;
  end;

Back to top