:: Birkhoff Theorem for Many Sorted Algebras
::  by Artur Korni{\l}owicz
::
:: Received June 19, 1997
:: Copyright (c) 1997-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, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE, MSUALG_3,
      REALSET1, MEMBER_1, FUNCT_6, TARSKI, FUNCT_1, WELLORD1, MSUALG_2,
      PRALG_2, CARD_3, SUBSET_1, MSUALG_5, MSUALG_4, FUNCOP_1, RLVECT_2,
      PRALG_1, EQREL_1, CLOSURE2, SETFAM_1, FUNCT_4, ZFMISC_1, GROUP_6,
      NUMBERS, EQUATION, ZF_MODEL, ZF_LANG, MCART_1, PZFMISC1, MSAFREE2,
      FINSET_1, BIRKHOFF;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, SETFAM_1, RELAT_1,
      XTUPLE_0, MCART_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1,
      FUNCT_2, FINSET_1, CARD_3, FUNCT_6, FUNCOP_1, MSUALG_1, MSUALG_2,
      PRALG_3, MSUALG_3, MSAFREE, MSAFREE2, PRALG_2, MSUALG_4, PZFMISC1,
      MSSUBFAM, CLOSURE2, MSUALG_5, EQUATION;
 constructors BINOP_1, PZFMISC1, MSSUBFAM, MSUALG_3, MSAFREE2, MSUALG_5,
      CLOSURE2, PRALG_3, EQUATION, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, PBOOLE,
      STRUCT_0, MSUALG_1, MSUALG_2, MSUALG_4, MSAFREE1, MSAFREE2, EXTENS_1,
      MSUALG_5, CLOSURE2, PRALG_3, MSUALG_9, EQUATION, MSSUBFAM, AUTALG_1,
      XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions FUNCT_1, RELAT_1, TARSKI, PBOOLE, PRALG_2, MSUALG_4, EQUATION,
      FUNCOP_1, PZFMISC1, XTUPLE_0;
 theorems CARD_3, CLOSURE2, EXTENS_1, FUNCOP_1, FUNCT_1, FUNCT_2, MCART_1,
      MSAFREE, MSAFREE2, MSSCYC_1, MSSUBFAM, MSUALG_2, MSUALG_3, MSUALG_4,
      MSUALG_5, MSUALG_7, MSUALG_9, PBOOLE, PRALG_2, PRALG_3, EQUATION,
      RELAT_1, ZFMISC_1, SETFAM_1;
 schemes DOMAIN_1, PBOOLE;

begin  :: Birkhoff Variety Theorem
::-------------------------------------------------------------------
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor Andrzej Trybulec
:: for his help in the preparation of the article.
::-------------------------------------------------------------------

definition
  let S be non empty non void ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, A be non-empty MSAlgebra over S, F be ManySortedFunction of X
  , the Sorts of A;
  func F-hash -> ManySortedFunction of FreeMSA X, A means
  : Def1:
  it is_homomorphism FreeMSA X, A & it || FreeGen X = F ** Reverse X;
  existence by MSAFREE:def 5;
  uniqueness by EXTENS_1:14;
end;

theorem Th1:
  for S being non empty non void ManySortedSign for A being
  non-empty MSAlgebra over S for X being non-empty ManySortedSet of the carrier
of S for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (
  F-hash)
proof
  let S be non empty non void ManySortedSign, A be non-empty MSAlgebra over S,
X be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of X,
  the Sorts of A;
  set R = Reverse X;
  let i be set;
  assume i in the carrier of S;
  then reconsider s = i as SortSymbol of S;
  let y be set;
A1: dom (R.s) = (FreeGen X).s by FUNCT_2:def 1;
  FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
  then
A2: (FreeGen X).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 2;
  assume y in (rngs F).i;
  then y in rng (F.s) by MSSUBFAM:13;
  then consider x being set such that
A3: x in dom (F.s) and
A4: y = F.s.x by FUNCT_1:def 3;
  rngs R = X by EXTENS_1:10;
  then R is "onto" by EXTENS_1:9;
  then rng (R.s) = X.s by MSUALG_3:def 3;
  then consider a being set such that
A5: a in dom (R.s) and
A6: x = R.s.a by A3,FUNCT_1:def 3;
A7: dom ((F-hash).s) = (the Sorts of FreeMSA X).s by FUNCT_2:def 1;
  y = (F.s*R.s).a by A4,A5,A6,FUNCT_1:13
    .= (F**R).s.a by MSUALG_3:2
    .= (F-hash || FreeGen X).s.a by Def1
    .= (((F-hash).s) | ((FreeGen X).s)).a by MSAFREE:def 1
    .= (F-hash).s.a by A5,FUNCT_1:49;
  then y in rng ((F-hash).s) by A5,A1,A7,A2,FUNCT_1:def 3;
  hence thesis by MSSUBFAM:13;
end;

:: Let P[] be a non empty abstract class of algebras. If P[] is closed under
:: subalgebras and products, the free algebras exist in P[].

scheme
  ExFreeAlg1 { S() -> non empty non void ManySortedSign, X() -> non-empty
MSAlgebra over S(), P[set] } : ex A being strict non-empty MSAlgebra over S(),
F being ManySortedFunction of X(), A st P[A] & F is_epimorphism X(), A & for B
being non-empty MSAlgebra over S() for G being ManySortedFunction of X(), B st
  G is_homomorphism X(), B & P[B] ex H being ManySortedFunction of A, B st H
is_homomorphism A, B & H ** F = G & for K being ManySortedFunction of A, B st K
  ** F = G holds H = K
provided
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: for I being set, F being MSAlgebra-Family of I, S() st (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product
F]
proof
  set EMF = the MSAlgebra-Family of {}, S();
  set CC = { C where C is Element of CongrLatt X() : ex R being MSCongruence
  of X() st R = C & P[QuotMSAlg (X(),R)] };
  set SF = the Sorts of X(), I = the carrier of S();
  consider Xi being ManySortedSet of I such that
A4: {Xi} = I --> {{}} by MSUALG_9:5;
  now
    let i be set;
    assume i in I;
    then reconsider s = i as SortSymbol of S();
    thus (the Sorts of product EMF).i = product Carrier(EMF,s) by
PRALG_2:def 10
      .= {{}} by CARD_3:10,PRALG_2:def 9
      .= (I --> {{}}).s by FUNCOP_1:7
      .= {Xi}.i by A4;
  end;
  then
A5: the Sorts of product EMF = {Xi} by PBOOLE:3;
  reconsider R = [|SF,SF|] as MSCongruence of X() by MSUALG_5:18;
  [|SF,SF|] is MSCongruence of X() by MSUALG_5:18;
  then
A6: [|SF,SF|] is Element of CongrLatt X() by MSUALG_5:def 6;
  the Sorts of QuotMSAlg (X(),R) = {SF} by MSUALG_9:29;
  then
A7: QuotMSAlg (X(),R), Trivial_Algebra S() are_isomorphic by MSUALG_9:26;
  for i being set st i in {} ex A being MSAlgebra over S() st A = EMF.i & P[A];
  then P[product EMF] by A3;
  then P[Trivial_Algebra S()] by A1,A5,MSUALG_9:26;
  then P[QuotMSAlg (X(),R)] by A1,A7,MSUALG_3:17;
  then
A8: [|SF,SF|] in CC by A6;
  defpred P[set,set] means ex R being MSCongruence of X() st R = $1 & $2 =
  QuotMSAlg (X(),R);
  defpred P1[set] means ex R being MSCongruence of X() st R = $1 & P[QuotMSAlg
  (X(),R)];
A9: now
    let q be set;
    assume q in CC;
    then
    ex C be Element of CongrLatt X() st q = C & ex R being MSCongruence
    of X() st R = C & P[QuotMSAlg (X(),R)];
    hence q is MSCongruence of X();
  end;
A10: CC c= the carrier of EqRelLatt SF
  proof
    let q be set;
    assume q in CC;
    then q is Equivalence_Relation of SF by A9;
    hence thesis by MSUALG_5:def 5;
  end;
  then reconsider CC as non empty SubsetFamily of [|SF,SF|] by A8,MSUALG_7:5;
  set R0 = meet |:CC:|;
A11: R0 is MSEquivalence_Relation-like ManySortedRelation of SF by A10,
MSUALG_7:8;
  reconsider R0 as ManySortedRelation of X() by A10,MSUALG_7:8;
  R0 is MSEquivalence-like
  proof
    let i be set, R be Relation of SF.i;
    assume that
A12: i in I and
A13: R0.i = R;
    thus thesis by A11,A12,A13,MSUALG_4:def 2;
  end;
  then reconsider R0 as MSEquivalence-like ManySortedRelation of X();
  { C where C is Element of CongrLatt X() : P1[C] } is Subset of CongrLatt
  X() from DOMAIN_1:sch 7;
  then reconsider R0 as MSCongruence of X() by MSUALG_9:28;
  take A = QuotMSAlg (X(),R0);
  reconsider F = MSNat_Hom(X(),R0) as ManySortedFunction of X(), A;
  take F;
A14: now
    let c be set;
    assume c in CC;
    then reconsider cc = c as MSCongruence of X() by A9;
    consider w being set such that
A15: w = QuotMSAlg (X(),cc);
    take w;
    thus P[c,w] by A15;
  end;
  consider FF being ManySortedSet of CC such that
A16: for c being set st c in CC holds P[c,FF.c] from PBOOLE:sch 3(A14);
  FF is MSAlgebra-Family of CC, S()
  proof
    let c be set;
    assume c in CC;
    then ex R being MSCongruence of X() st R = c & FF.c = QuotMSAlg (X(),R)
    by A16;
    hence thesis;
  end;
  then reconsider FF as MSAlgebra-Family of CC, S();
  defpred P[Element of CC,set] means ex F1 being ManySortedFunction of X(),FF.
  $1 st F1 = $2 & F1 is_homomorphism X(),FF.$1 & ex R being MSCongruence of X()
  st $1 = R & F1 = MSNat_Hom(X(),R);
A17: for c being Element of CC ex j being set st P[c,j]
  proof
    let c be Element of CC;
    consider R being MSCongruence of X() such that
A18: R = c and
A19: FF.c = QuotMSAlg (X(),R) by A16;
    set j = MSNat_Hom(X(),R);
    reconsider F1 = j as ManySortedFunction of X(),FF.c by A19;
    take j;
    take F1;
    thus F1 = j;
    MSNat_Hom(X(),R) is_epimorphism X(),QuotMSAlg (X(),R) by MSUALG_4:3;
    hence F1 is_homomorphism X(),FF.c by A19,MSUALG_3:def 8;
    take R;
    thus thesis by A18;
  end;
  consider FofI1 being ManySortedSet of CC such that
A20: for c being Element of CC holds P[c,FofI1.c] from PBOOLE:sch 6(A17);
A21: for c being Element of CC ex F1 being ManySortedFunction of X(),FF.c st
  F1 = FofI1.c & F1 is_homomorphism X(),FF.c
  proof
    let c be Element of CC;
    consider F1 being ManySortedFunction of X(),FF.c such that
A22: F1 = FofI1.c and
A23: F1 is_homomorphism X(),FF.c and
    ex R being MSCongruence of X() st c = R & F1 = MSNat_Hom(X(),R) by A20;
    take F1;
    thus thesis by A22,A23;
  end;
  FofI1 is Function-yielding
  proof
    let c be set;
    assume c in dom FofI1;
    then reconsider cc = c as Element of CC;
    ex F1 being ManySortedFunction of X(),FF.cc st F1 = FofI1. cc & F1
    is_homomorphism X(),FF.cc by A21;
    hence thesis;
  end;
  then reconsider FofI1 as ManySortedFunction of CC;
  consider H being ManySortedFunction of X(),product FF such that
A24: H is_homomorphism X(),product FF and
A25: for c being Element of CC holds proj(FF,c) ** H = FofI1.c by A21,
PRALG_3:29;
  now
    let i be set;
    assume i in I;
    then reconsider s = i as SortSymbol of S();
    consider Q being Subset-Family of ([|SF,SF|].s) such that
A26: Q = |:CC:|.s and
A27: (meet |:CC:|).s = Intersect Q by MSSUBFAM:def 1;
A28: |:CC:|.s = { t.s where t is Element of Bool [|SF,SF|] : t in CC } by
CLOSURE2:14;
    (MSCng H).s = R0.s
    proof
      let a, b be set;
      hereby
        assume
A29:    [a,b] in (MSCng H).s;
        then
A30:    a in SF.s by ZFMISC_1:87;
A31:    b in SF.s by A29,ZFMISC_1:87;
A32:    [a,b] in MSCng (H,s) by A24,A29,MSUALG_4:def 18;
A33:    for Y being set st Y in Q holds [a,b] in Y
        proof
          let Y be set;
          assume Y in Q;
          then consider t being Element of Bool [|SF,SF|] such that
A34:      Y = t.s and
A35:      t in CC by A26,A28;
          reconsider t1 = t as Element of CC by A35;
          consider F1 being ManySortedFunction of X(),FF.t1 such that
A36:      F1 = FofI1.t1 and
          F1 is_homomorphism X(),FF.t1 and
A37:      ex R being MSCongruence of X() st t1 = R & F1 = MSNat_Hom(X
          (),R) by A20;
          F1.s.a = (proj(FF,t1) ** H).s.a by A25,A36
            .= ((proj(FF,t1)).s * H.s).a by MSUALG_3:2
            .= (proj(FF,t1).s).((H.s).a) by A30,FUNCT_2:15
            .= (proj(FF,t1).s).((H.s).b) by A30,A31,A32,MSUALG_4:def 17
            .= ((proj(FF,t1)).s * H.s).b by A31,FUNCT_2:15
            .= (proj(FF,t1) ** H).s.b by MSUALG_3:2
            .= F1.s.b by A25,A36;
          hence thesis by A30,A31,A34,A37,MSUALG_9:33;
        end;
        [a,b] in [:SF.s,SF.s:] by A29;
        then [a,b] in [|SF,SF|].s by PBOOLE:def 16;
        hence [a,b] in R0.s by A27,A33,SETFAM_1:43;
      end;
      assume
A38:  [a,b] in R0.s;
      then
A39:  a in SF.s by ZFMISC_1:87;
A40:  b in SF.s by A38,ZFMISC_1:87;
A41:  for c being Element of CC holds proj(Carrier(FF,s),c).(H.s.a) =
      proj(Carrier(FF,s),c).(H.s.b)
      proof
        let c be Element of CC;
        reconsider t1 = c as MSCongruence of X() by A9;
        consider F1 being ManySortedFunction of X(),FF.c such that
A42:    F1 = FofI1.c and
        F1 is_homomorphism X(),FF.c and
A43:    ex R being MSCongruence of X() st c = R & F1 = MSNat_Hom(X(),
        R) by A20;
        t1 is Element of Bool [|SF,SF|] by CLOSURE2:def 1;
        then t1.s in |:CC:|.s by A28;
        then
A44:    [a,b] in t1.s by A26,A27,A38,SETFAM_1:43;
        thus proj(Carrier(FF,s),c).(H.s.a) = (proj(FF,c).s).(H.s.a) by
PRALG_3:def 2
          .= ((proj(FF,c)).s * H.s).a by A39,FUNCT_2:15
          .= (proj(FF,c) ** H).s.a by MSUALG_3:2
          .= F1.s.a by A25,A42
          .= F1.s.b by A39,A40,A44,A43,MSUALG_9:33
          .= (proj(FF,c) ** H).s.b by A25,A42
          .= ((proj(FF,c)).s * H.s).b by MSUALG_3:2
          .= (proj(FF,c).s).(H.s.b) by A40,FUNCT_2:15
          .= proj(Carrier(FF,s),c).(H.s.b) by PRALG_3:def 2;
      end;
      H.s.b in (the Sorts of product FF).s by A40,FUNCT_2:5;
      then
A45:  H.s.b in product Carrier(FF,s) by PRALG_2:def 10;
      H.s.a in (the Sorts of product FF).s by A39,FUNCT_2:5;
      then H.s.a in product Carrier(FF,s) by PRALG_2:def 10;
      then H.s.a = H.s.b by A45,A41,MSUALG_9:14;
      then [a,b] in MSCng (H,s) by A39,A40,MSUALG_4:def 17;
      hence thesis by A24,MSUALG_4:def 18;
    end;
    hence (MSCng H).i = R0.i;
  end;
  then
A46: MSCng H = R0 by PBOOLE:3;
  QuotMSAlg (X(),MSCng H), Image MSHomQuot H are_isomorphic by A24,MSUALG_4:4
,MSUALG_9:16;
  then consider XX being strict non-empty MSSubAlgebra of product FF such that
A47: A, XX are_isomorphic by A46;
  for cc being set st cc in CC ex A being MSAlgebra over S() st A = FF.cc
  & P[A]
  proof
    let cc be set;
    assume
A48: cc in CC;
    then reconsider c = cc as Element of CC;
    take FF.c;
A49: ex C be Element of CongrLatt X() st cc = C & ex R being
    MSCongruence of X() st R = C & P[QuotMSAlg (X(),R)] by A48;
    ex R being MSCongruence of X() st R = cc & FF.cc = QuotMSAlg (X(),R
    ) by A16,A48;
    hence thesis by A49;
  end;
  then P[XX] by A2,A3;
  hence P[A] by A1,A47,MSUALG_3:17;
  thus F is_epimorphism X(), A by MSUALG_4:3;
  then
A50: F is "onto" by MSUALG_3:def 8;
  let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), B
  such that
A51: G is_homomorphism X(), B and
A52: P[B];
  reconsider C = Image MSHomQuot G as strict non-empty MSSubAlgebra of B;
A53: QuotMSAlg (X(),MSCng G), C are_isomorphic by A51,MSUALG_4:4,MSUALG_9:16;
A54: MSCng G is Element of CongrLatt X() by MSUALG_5:def 6;
  P[C] by A2,A52;
  then P[QuotMSAlg (X(),MSCng G)] by A1,A53,MSUALG_3:17;
  then MSCng(G) in CC by A54;
  then R0 c= MSCng(G) by CLOSURE2:21,MSSUBFAM:43;
  then consider H being ManySortedFunction of A, B such that
A55: H is_homomorphism A, B and
A56: G = H ** F by A51,MSUALG_9:36;
  take H;
  thus H is_homomorphism A, B by A55;
  thus G = H ** F by A56;
  let K be ManySortedFunction of A, B;
  assume K ** F = G;
  hence thesis by A56,A50,EXTENS_1:12;
end;

scheme
  ExFreeAlg2 { S() -> non empty non void ManySortedSign, X() -> non-empty
  ManySortedSet of the carrier of S(), P[set] } : ex A being strict non-empty
MSAlgebra over S(), F being ManySortedFunction of X(), the Sorts of A st P[A] &
for B being non-empty MSAlgebra over S() for G being ManySortedFunction of X(),
  the Sorts of B st P[B] ex H being ManySortedFunction of A, B st H
is_homomorphism A, B & H ** F = G & for K being ManySortedFunction of A, B st K
  is_homomorphism A, B & K ** F = G holds H = K
provided
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: for I being set, F being MSAlgebra-Family of I, S() st (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product
F]
proof
A4: for A being non-empty MSAlgebra over S() for B being strict non-empty
  MSSubAlgebra of A st P[A] holds P[B] by A2;
A5: for I being set, F being MSAlgebra-Family of I, S() st (for i being set
  st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]
  by A3;
  set FM = FreeMSA X();
A6: Reverse X() is "1-1" by MSUALG_9:11;
A7: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
  ] holds P[B] by A1;
  consider A being strict non-empty MSAlgebra over S(), F being
  ManySortedFunction of FM, A such that
A8: P[A] and
A9: F is_epimorphism FM, A and
A10: for B being non-empty MSAlgebra over S() for G being
  ManySortedFunction of FM, B st G is_homomorphism FM, B & P[B] ex H being
ManySortedFunction of A, B st H is_homomorphism A, B & H ** F = G & for K being
ManySortedFunction of A, B st K ** F = G holds H = K from ExFreeAlg1(A7,A4,A5);
  reconsider R = (F || FreeGen X()) ** ((Reverse X())"") as ManySortedFunction
  of X(), the Sorts of A;
  take A;
  take R;
  thus P[A] by A8;
  let B be non-empty MSAlgebra over S(), G be ManySortedFunction of X(), the
  Sorts of B such that
A11: P[B];
  consider GG being ManySortedFunction of FM, B such that
A12: GG is_homomorphism FM, B and
A13: GG || FreeGen X() = G ** Reverse X() by MSAFREE:def 5;
  consider H being ManySortedFunction of A, B such that
A14: H is_homomorphism A, B and
A15: H ** F = GG and
  for K being ManySortedFunction of A, B st K ** F = GG holds H = K by A10,A11
,A12;
  take H;
  thus H is_homomorphism A, B by A14;
A16: H ** (F || FreeGen X()) = GG || FreeGen X() by A15,EXTENS_1:4;
A17: F is "onto" by A9,MSUALG_3:def 8;
  rngs Reverse X() = X() by EXTENS_1:10;
  then
A18: Reverse X() is "onto" by EXTENS_1:9;
  R ** Reverse X() = (F || FreeGen X()) ** (((Reverse X())"")**Reverse X(
  )) by PBOOLE:140
    .= (F || FreeGen X()) ** (id FreeGen X()) by A18,A6,MSUALG_3:5
    .= F || FreeGen X() by MSUALG_3:3;
  then
A19: H ** R ** Reverse X() = G ** Reverse X() by A13,A16,PBOOLE:140;
  hence H ** R = G by A18,EXTENS_1:12;
  let K be ManySortedFunction of A, B;
  assume
A20: K is_homomorphism A, B;
  assume K ** R = G;
  then
  K ** (((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) = H** (
  (F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X() by A19,PBOOLE:140;
  then
  K ** (((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) = H** (
  ((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) by PBOOLE:140;
  then
  K ** ((F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) = H** (
  ((F || FreeGen X()) ** ((Reverse X())"")) ** Reverse X()) by PBOOLE:140;
  then
  K ** ((F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) = H** (
  (F || FreeGen X()) ** (((Reverse X()"")) ** Reverse X())) by PBOOLE:140;
  then K ** (F || FreeGen X() ** id FreeGen X()) = H** ((F || FreeGen X()) **
  (((Reverse X()"")) ** Reverse X())) by A18,A6,MSUALG_3:5;
  then
  K ** (F || FreeGen X() ** id FreeGen X()) = H** (F || FreeGen X() ** id
  FreeGen X()) by A18,A6,MSUALG_3:5;
  then K ** (F || FreeGen X()) = H** (F || FreeGen X() ** id FreeGen X()) by
MSUALG_3:3;
  then K ** (F || FreeGen X()) = H** (F || FreeGen X()) by MSUALG_3:3;
  then (K ** F) || FreeGen X() = H** (F || FreeGen X()) by EXTENS_1:4;
  then
A21: (K ** F) || FreeGen X() = (H** F) || FreeGen X() by EXTENS_1:4;
  F is_homomorphism FM, A by A9,MSUALG_3:def 8;
  then K ** F is_homomorphism FM, B by A20,MSUALG_3:10;
  then K ** F = H ** F by A12,A15,A21,EXTENS_1:14;
  hence thesis by A17,EXTENS_1:12;
end;

scheme
  Exhash { S() -> non empty non void ManySortedSign, F, A() -> non-empty
MSAlgebra over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of F(), a() -> ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of A(), P[set] } : ex H being ManySortedFunction of F(), A() st H
  is_homomorphism F(), A() & a()-hash = H ** (fi()-hash)
provided
A1: P[A()] and
A2: for C being non-empty MSAlgebra over S() :: F() is free in P[]
for G being ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of C st P[C] ex h being ManySortedFunction of F(), C st
  h is_homomorphism F(), C & G = h ** fi()
proof
  consider H being ManySortedFunction of F(), A() such that
A3: H is_homomorphism F(), A() and
A4: a() = H ** fi() by A1,A2;
  take H;
  thus H is_homomorphism F(), A() by A3;
  fi()-hash is_homomorphism FreeMSA ((the carrier of S()) --> NAT), F() by Def1
;
  then
A5: H ** (fi()-hash) is_homomorphism FreeMSA ((the carrier of S()) --> NAT),
  A() by A3,MSUALG_3:10;
  reconsider SN = (the carrier of S()) --> NAT as non-empty ManySortedSet of
  the carrier of S();
  reconsider h1 = a() as ManySortedFunction of SN, the Sorts of A();
A6: h1-hash is_homomorphism FreeMSA SN, A() by Def1;
  h1-hash || FreeGen SN = a() ** Reverse SN by Def1
    .= H ** (fi() ** Reverse SN) by A4,PBOOLE:140
    .= H ** (fi()-hash || FreeGen ((the carrier of S()) --> NAT)) by Def1
    .= (H ** (fi()-hash)) || FreeGen ((the carrier of S()) --> NAT) by
EXTENS_1:4;
  hence thesis by A6,A5,EXTENS_1:14;
end;

:: Let P[] be a class of algebras. If a free algebra F() in P[]
:: relative to fi() exists, then
:: P[] |= [t1(),t2()]  iff  (F(),fi()) |= [t1(),t2()].

scheme
  EqTerms { S() -> non empty non void ManySortedSign, F() -> non-empty
MSAlgebra over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of F(), s() -> SortSymbol of S(), t1, t2() -> Element of (the Sorts
of TermAlg S()).s(), P[set] } : for B being non-empty MSAlgebra over S() st P[B
  ] holds B |= t1() '=' t2()
provided
A1: fi()-hash.s().t1() = fi()-hash.s().t2() and
A2: for C being non-empty MSAlgebra over S() for G being
ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex h
being ManySortedFunction of F(), C st h is_homomorphism F(), C & G = h ** fi()
proof
  reconsider fi1 = fi() as ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of F();
  reconsider SN = (the carrier of S()) --> NAT as non-empty ManySortedSet of (
  the carrier of S());
  let B be non-empty MSAlgebra over S();
  assume P[B];
  then
A3: P[B];
  let h be ManySortedFunction of TermAlg S(), B such that
A4: h is_homomorphism TermAlg S(), B;
  reconsider h1 = h as ManySortedFunction of FreeMSA SN, B;
  set alfa = (h1 || FreeGen SN) ** ((Reverse SN)"");
A5: alfa-hash is_homomorphism FreeMSA SN, B by Def1;
  reconsider alfa1 = alfa as ManySortedFunction of (the carrier of S()) -->
  NAT, the Sorts of B;
A6: for C being non-empty MSAlgebra over S() for G being ManySortedFunction
  of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex h being
ManySortedFunction of F(), C st h is_homomorphism F(), C & G = h ** fi1 by A2;
  consider H being ManySortedFunction of F(), B such that
  H is_homomorphism F(), B and
A7: alfa1-hash = H ** (fi1-hash) from Exhash(A3,A6);
A8: alfa-hash.s().t1() = (H.s() * (fi()-hash).s()).t1() by A7,MSUALG_3:2
    .= H.s().(fi()-hash.s().t2()) by A1,FUNCT_2:15
    .= (H.s() * (fi()-hash).s()).t2() by FUNCT_2:15
    .= alfa-hash.s().t2() by A7,MSUALG_3:2;
  rngs Reverse SN = SN by EXTENS_1:10;
  then
A9: Reverse SN is "1-1" "onto" by EXTENS_1:9,MSUALG_9:11;
  alfa-hash || FreeGen SN = alfa ** Reverse SN by Def1
    .= (h1 || FreeGen SN) ** (((Reverse SN)"") ** Reverse SN) by PBOOLE:140
    .= (h1 || FreeGen SN) ** id FreeGen SN by A9,MSUALG_3:5
    .= h1 || FreeGen SN by MSUALG_3:3;
  then
A10: alfa-hash = h1 by A4,A5,EXTENS_1:14;
  thus h.s().([t1(),t2()]`1) = h.s().t1()
    .= h.s().([t1(),t2()]`2) by A10,A8;
end;

:: Let P[] be an abstract class of algebras such that P[] is closed under
:: subalgebras. The free algebra in P[] over X(), if it exists,
:: is generated by X().

scheme
  FreeIsGen { S() -> non empty non void ManySortedSign, X() -> non-empty
ManySortedSet of the carrier of S(), A() -> strict non-empty MSAlgebra over S()
, f() -> ManySortedFunction of X(), the Sorts of A(), P[set] } : f().:.:X() is
  non-empty GeneratorSet of A()
provided
A1: for C being non-empty MSAlgebra over S() :: A() is free in P[]
for G being ManySortedFunction of X(), the Sorts of C st P[C]
 ex H being ManySortedFunction of A(), C st
   H is_homomorphism A(), C & H ** f() = G &
   for K being ManySortedFunction of A(), C st
     K is_homomorphism A(), C & K ** f() = G holds H = K and
A2: P[A()] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B]
proof
  set I = the carrier of S ();
A4: f().:.:X() is non-empty
  proof
    let i be set;
    assume
A5: i in I;
    then reconsider fi = f().i as Function of X().i, (the Sorts of A()).i by
PBOOLE:def 15;
A6: (f().:.:X()).i = fi.:(X().i) by A5,PBOOLE:def 20;
    reconsider Xi = X().i as non empty set by A5;
A7: Xi meets Xi;
    dom fi = Xi by A5,FUNCT_2:def 1;
    hence thesis by A7,A6,RELAT_1:118;
  end;
  f().:.:X() is ManySortedSubset of the Sorts of A()
  proof
    let i be set;
    assume
A8: i in I;
    then reconsider fi = f().i as Function of X().i, (the Sorts of A()).i by
PBOOLE:def 15;
    (f().:.:X()).i = fi.:(X().i) by A8,PBOOLE:def 20;
    hence thesis;
  end;
  then reconsider Gen = f().:.:X() as non-empty MSSubset of A() by A4;
  set AA = GenMSAlg Gen;
A9: X() is_transformable_to the Sorts of AA
  proof
    let i be set;
    assume i in I;
    hence thesis;
  end;
  X() is_transformable_to the Sorts of A()
  proof
    let i be set;
    assume i in I;
    hence thesis;
  end;
  then
A10: doms f() = X() by MSSUBFAM:17;
  then rngs f() = f().:.:X() by EQUATION:13;
  then rngs f() is ManySortedSubset of the Sorts of AA by MSUALG_2:def 17;
  then rngs f() c= the Sorts of AA by PBOOLE:def 18;
  then reconsider
  iN = f() as ManySortedFunction of X(), the Sorts of AA by A9,A10,EQUATION:4;
  consider IN being ManySortedFunction of A(), AA such that
A11: IN is_homomorphism A(), AA and
A12: IN ** f() = iN and
  for K being ManySortedFunction of A(), AA st K is_homomorphism A(), AA &
  K ** f() = iN holds IN = K by A1,A2,A3;
  the Sorts of AA is ManySortedSubset of the Sorts of A() by MSUALG_2:def 9;
  then reconsider h = id the Sorts of AA as ManySortedFunction of AA, A() by
EXTENS_1:5;
  consider HIN being ManySortedFunction of A(), A() such that
  HIN is_homomorphism A(), A() and
  HIN ** f() = h ** iN and
A13: for K being ManySortedFunction of A(), A() st K is_homomorphism A()
  , A() & K ** f() = h ** iN holds HIN = K by A1,A2;
  h is_monomorphism AA, A() by MSUALG_3:22;
  then
A14: h is_homomorphism AA, A() by MSUALG_3:def 9;
  reconsider hIN = h ** IN as ManySortedFunction of A(), A();
  h ** iN = (h ** IN) ** f() by A12,PBOOLE:140;
  then
A15: HIN = hIN by A11,A13,A14,MSUALG_3:10;
A16: A() is MSSubAlgebra of A() by MSUALG_2:5;
  f() = h ** iN by MSUALG_3:4;
  then (id the Sorts of A()) ** f() = h ** iN by MSUALG_3:4;
  then HIN = id the Sorts of A() by A13,MSUALG_3:9;
  then
A17: HIN is "onto";
  the Sorts of AA = h.:.:(the Sorts of AA) by EQUATION:15
    .= the Sorts of A() by A15,A17,EQUATION:2,9;
  then AA = A() by A16,MSUALG_2:9;
  hence thesis by MSAFREE:3;
end;

scheme
  Hashisonto { S() -> non empty non void ManySortedSign, A() -> strict
non-empty MSAlgebra over S(), F() -> ManySortedFunction of (the carrier of S())
  --> NAT, the Sorts of A(), P[set] } : F()-hash is_epimorphism FreeMSA ((the
  carrier of S()) --> NAT), A()
provided
A1: for C being non-empty MSAlgebra over S() for G being
ManySortedFunction of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex H
being ManySortedFunction of A(), C st H is_homomorphism A(), C & H ** F() = G &
for K being ManySortedFunction of A(), C st K is_homomorphism A(), C & K ** F()
= G holds H = K and
A2: P[A()] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B]
proof
A4: P[A()] by A2;
  set V = (the carrier of S()) --> NAT;
  reconsider Gen = the Sorts of FreeMSA V as GeneratorSet of FreeMSA V by
MSAFREE2:6;
A5: F().:.:V c= rngs F() by EQUATION:12;
  the Sorts of FreeMSA V is_transformable_to the Sorts of A()
  proof
    let i be set such that
A6: i in the carrier of S();
    assume (the Sorts of A()).i = {};
    hence thesis by A6;
  end;
  then doms (F()-hash) = the Sorts of FreeMSA V by MSSUBFAM:17;
  then
A7: F()-hash.:.:(the Sorts of FreeMSA V) = rngs (F()-hash) by EQUATION:13;
  rngs F() c= rngs (F()-hash) by Th1;
  then
A8: F().:.:V c= F()-hash.:.:Gen by A7,A5,PBOOLE:13;
A9: F()-hash is_homomorphism FreeMSA V, A() by Def1;
A10: for A being non-empty MSAlgebra over S() for B being strict non-empty
  MSSubAlgebra of A st P[A] holds P[B] by A3;
A11: for C being non-empty MSAlgebra over S() for G being ManySortedFunction
  of (the carrier of S()) --> NAT, the Sorts of C st P[C] ex H being
ManySortedFunction of A(), C st H is_homomorphism A(), C & H ** F() = G & for K
  being ManySortedFunction of A(), C st K is_homomorphism A(), C & K ** F() = G
  holds H = K by A1;
  F().:.:V is non-empty GeneratorSet of A() from FreeIsGen(A11,A4,A10);
  hence thesis by A8,A9,EQUATION:23;
end;

scheme
  FinGenAlgInVar { S() -> non empty non void ManySortedSign, A() -> strict
  finitely-generated non-empty MSAlgebra over S(), F() -> non-empty MSAlgebra
over S(), fi() -> ManySortedFunction of (the carrier of S()) --> NAT, the Sorts
  of F(), P, Q[set] } : P[A()]
provided
A1: Q[A()] and
A2: P[F()] and
A3: for C being non-empty MSAlgebra over S() :: F() is free in Q[]
for G being ManySortedFunction of (the carrier of S()) --> NAT,
  the Sorts of C st Q[C] ex h being ManySortedFunction of F(), C st
  h is_homomorphism F(), C & G = h ** fi() and
A4: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A5: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)]
proof
  set I = the carrier of S(), sA = the Sorts of A();
  consider Gen being GeneratorSet of A() such that
A6: Gen is finite-yielding by MSAFREE2:def 10;
  reconsider Gen as finite-yielding ManySortedSubset of sA by A6;
  consider GEN being non-empty finite-yielding ManySortedSubset of sA such
  that
A7: Gen c= GEN by MSUALG_9:7;
  consider F being ManySortedFunction of I --> NAT, GEN such that
A8: F is "onto" by MSUALG_9:12;
  I --> NAT is_transformable_to GEN
  proof
    let i be set;
    assume i in I;
    hence thesis;
  end;
  then reconsider G = F as ManySortedFunction of I --> NAT, sA by EXTENS_1:5;
  consider h being ManySortedFunction of F(), A() such that
A9: h is_homomorphism F(), A() and
A10: G = h ** fi() by A1,A3;
  reconsider sI1 = the Sorts of Image h as MSSubset of Image h by PBOOLE:def 18
;
A11: GEN is GeneratorSet of A() by A7,MSSCYC_1:21;
  reconsider sI = the Sorts of Image h as MSSubset of A() by MSUALG_2:def 9;
  GEN is ManySortedSubset of sI
  proof
    let i be set;
    assume i in I;
    then reconsider s = i as SortSymbol of S();
    let g be set;
    assume
A12: g in GEN.i;
A13: (I --> NAT).s = NAT by FUNCOP_1:7;
    then reconsider fi = fi().s as Function of NAT, (the Sorts of F()).s;
    dom ((h.s)*fi) = NAT by FUNCT_2:def 1
      .= dom fi by FUNCT_2:def 1;
    then
A14: rng fi c= dom (h.s) by FUNCT_1:15;
    rng (F.s) = GEN.s by A8,MSUALG_3:def 3;
    then consider x being set such that
A15: x in dom (F.s) and
A16: g = F.s.x by A12,FUNCT_1:def 3;
    dom (F.s) = NAT by A13,FUNCT_2:def 1
      .= dom fi by FUNCT_2:def 1;
    then
A17: fi.x in rng fi by A15,FUNCT_1:def 3;
    g = ((h.s)*fi).x by A10,A16,MSUALG_3:2
      .= (h.s).(fi.x) by A15,FUNCT_2:15;
    then g in (h.s).:((the Sorts of F()).s) by A17,A14,FUNCT_1:def 6;
    then g in (h.:.:(the Sorts of F())).s by PBOOLE:def 20;
    hence thesis by A9,MSUALG_3:def 12;
  end;
  then
A18: GenMSAlg GEN is MSSubAlgebra of GenMSAlg sI by EXTENS_1:17;
  GenMSAlg sI = GenMSAlg sI1 by EXTENS_1:18;
  then GenMSAlg GEN is MSSubAlgebra of Image h by A18,MSUALG_2:21;
  then A() is MSSubAlgebra of Image h by A11,MSAFREE:3;
  then A() = Image h by MSUALG_2:7;
  then
A19: h is_epimorphism F(), A() by A9,MSUALG_3:19;
  P[QuotMSAlg (F(),MSCng h)] by A2,A5;
  hence thesis by A4,A19,MSUALG_4:6;
end;

scheme
  QuotEpi { S() -> non empty non void ManySortedSign, X, Y() -> non-empty
  MSAlgebra over S(), P[set] } : P[Y()]
provided
A1: ex H being ManySortedFunction of X(), Y() st H is_epimorphism X(), Y () and
A2: P[X()] and
A3: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A4: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)]
proof
  consider H being ManySortedFunction of X(), Y() such that
A5: H is_epimorphism X(), Y() by A1;
  P[QuotMSAlg (X(),MSCng H)] by A2,A4;
  hence thesis by A3,A5,MSUALG_4:6;
end;

:: An algebra X() belongs to a variety P[] whenever all its finitely
:: generated subalgebras are in P[].

scheme
  AllFinGen { S() -> non empty non void ManySortedSign, X() -> non-empty
  MSAlgebra over S(), P[set] } : P[X()]
provided
A1: for B being strict non-empty finitely-generated MSSubAlgebra of X()
holds P[B] and
A2: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A3: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A4: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)] and
A5: for I being set, F being MSAlgebra-Family of I, S() st (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product
F]
proof
A6: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[
  A] holds P[B] by A2;
  set T = the strict non-empty finitely-generated MSSubAlgebra of X();
  set CC = { C where C is Element of MSSub X() : ex R being strict non-empty
  finitely-generated MSSubAlgebra of X() st R = C };
  T in MSSub X() by MSUALG_2:def 19;
  then T in CC;
  then reconsider CC as non empty set;
  defpred P[set,set] means $1 = $2;
A7: for c being set st c in CC ex j being set st P[c,j];
  consider FF being ManySortedSet of CC such that
A8: for c being set st c in CC holds P[c,FF.c] from PBOOLE:sch 3(A7);
  FF is MSAlgebra-Family of CC, S()
  proof
    let c be set;
    assume
A9: c in CC;
    then ex Q being Element of MSSub X() st c = Q & ex R being strict
    non-empty finitely-generated MSSubAlgebra of X() st R = Q;
    hence thesis by A8,A9;
  end;
  then reconsider FF as MSAlgebra-Family of CC, S();
  consider prSOR being strict non-empty MSSubAlgebra of product FF such that
A10: ex BA being ManySortedFunction of prSOR, X() st BA is_epimorphism
  prSOR, X() by A8,EQUATION:27;
A11: for A being non-empty MSAlgebra over S(), R being MSCongruence of A st
  P[A] holds P[QuotMSAlg (A,R)] by A4;
  for i being set st i in CC ex A being MSAlgebra over S() st A = FF.i & P[A]
  proof
    let i be set;
    assume
A12: i in CC;
    then consider Q being Element of MSSub X() such that
A13: i = Q and
A14: ex R being strict non-empty finitely-generated MSSubAlgebra of X(
    ) st R = Q;
    consider R being strict non-empty finitely-generated MSSubAlgebra of X()
    such that
A15: R = Q by A14;
    take R;
    thus thesis by A1,A8,A12,A13,A15;
  end;
  then
A16: P[prSOR] by A3,A5;
  thus P[X()] from QuotEpi(A10, A16, A6, A11);
end;

scheme
  FreeInModIsInVar1 { S() -> non empty non void ManySortedSign, X() ->
  non-empty MSAlgebra over S(), P, Q[set] } : Q[X()]
provided
A1: for A being non-empty MSAlgebra over S() holds Q[A] iff for s being
SortSymbol of S(), e being Element of (Equations S()).s st (for B being
non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e and
A2: P[X()]
proof
  for s being SortSymbol of S(), e being Element of (Equations S()).s st (
  for B being non-empty MSAlgebra over S() st P[B] holds B |= e) holds X() |= e
  by A2;
  hence thesis by A1;
end;

:: If P[] is a non empty variety, then the free algebras in Mod Eq P[]
:: belong to P[].   (Q[] = Mod Eq P[])

scheme
  FreeInModIsInVar { S() -> non empty non void ManySortedSign, X() -> strict
non-empty MSAlgebra over S(), psi() -> ManySortedFunction of (the carrier of S(
  )) --> NAT, the Sorts of X(), P, Q[set] } : P[X()]
provided
A1: for A being non-empty MSAlgebra over S() holds Q[A] iff for s being
SortSymbol of S(), e being Element of (Equations S()).s st (for B being
non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e and
A2: for C being non-empty MSAlgebra over S() :: X() is free in Q[]
 for G being ManySortedFunction of (the carrier of S()) --> NAT,
 the Sorts of C st Q[C] ex H being ManySortedFunction of X(), C st
 H is_homomorphism X(), C & H ** psi() = G
 & for K being ManySortedFunction of X(), C st
 K is_homomorphism X(), C & K ** psi() = G holds H = K and
A3: Q[X()] and
A4: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A5: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A6: for I being set, F being MSAlgebra-Family of I, S() st (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product
F]
proof
A7: for I being set, F being MSAlgebra-Family of I, S() st (for i being set
  st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]
  by A6;
  set V = (the carrier of S()) --> NAT;
A8: for A being non-empty MSAlgebra over S() for B being strict non-empty
  MSSubAlgebra of A st P[A] holds P[B] by A5;
A9: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
  ] holds P[B] by A4;
  consider A being strict non-empty MSAlgebra over S(), fi being
  ManySortedFunction of V, the Sorts of A such that
A10: P[A] and
A11: for B being non-empty MSAlgebra over S() for G being
  ManySortedFunction of V, the Sorts of B st P[B] ex H being ManySortedFunction
  of A, B st H is_homomorphism A, B & H ** fi = G & for K being
ManySortedFunction of A, B st K is_homomorphism A, B & K ** fi = G holds H = K
  from ExFreeAlg2(A9,A8, A7);
A12: for C being non-empty MSAlgebra over S() for G being ManySortedFunction
  of (the carrier of S()) --> NAT, the Sorts of C st Q[C] ex H being
ManySortedFunction of X(), C st H is_homomorphism X(), C & H ** psi() = G & for
K being ManySortedFunction of X(), C st K is_homomorphism X(), C & K ** psi() =
  G holds H = K by A2;
A13: for C being non-empty MSAlgebra over S() for G being ManySortedFunction
  of (the carrier of S()) --> NAT, the Sorts of C st Q[C] ex h being
  ManySortedFunction of X(), C st h is_homomorphism X(), C & G = h ** psi()
  proof
    let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V, the
    Sorts of C;
    assume Q[C];
    then consider h being ManySortedFunction of X(), C such that
A14: h is_homomorphism X(), C and
A15: G = h ** psi() and
    for K being ManySortedFunction of X(), C st K is_homomorphism X(), C &
    K ** psi() = G holds h = K by A2;
    take h;
    thus thesis by A14,A15;
  end;
A16: Q[X()] by A3;
A17: for A being non-empty MSAlgebra over S() holds Q[A] iff for s being
  SortSymbol of S(), e being Element of (Equations S()).s st (for B being
  non-empty MSAlgebra over S() st P[B] holds B |= e) holds A |= e by A1;
A18: Q[A] from FreeInModIsInVar1(A17,A10);
  consider H being ManySortedFunction of X(), A such that
A19: H is_homomorphism X(), A and
A20: fi-hash = H ** (psi()-hash) from Exhash(A18,A13);
A21: psi()-hash is_homomorphism FreeMSA V, X() by Def1;
  now
    let i be set;
    assume i in the carrier of S();
    then reconsider s = i as SortSymbol of S();
    thus H.i is one-to-one
    proof
A22:  for D being non-empty MSAlgebra over S() for E being strict
      non-empty MSSubAlgebra of D holds Q[D] implies Q[E]
      proof
        let D be non-empty MSAlgebra over S(), E be strict non-empty
        MSSubAlgebra of D such that
A23:    Q[D];
        now
          let s be SortSymbol of S(), e be Element of (Equations S()).s;
          assume for B being non-empty MSAlgebra over S() st P[B] holds B |= e;
          then D |= e by A1,A23;
          hence E |= e by EQUATION:31;
        end;
        hence thesis by A1;
      end;
      psi()-hash is_epimorphism FreeMSA V, X() from Hashisonto(A12, A16,
      A22);
      then
A24:  psi()-hash is "onto" by MSUALG_3:def 8;
A25:  for C being non-empty MSAlgebra over S() for G being
ManySortedFunction of V, the Sorts of C st P[C] ex H being ManySortedFunction
      of A, C st H is_homomorphism A, C & G = H ** fi
      proof
        let C be non-empty MSAlgebra over S(), G be ManySortedFunction of V,
        the Sorts of C;
        assume P[C];
        then consider H being ManySortedFunction of A, C such that
A26:    H is_homomorphism A, C and
A27:    H ** fi = G and
        for K being ManySortedFunction of A, C st K is_homomorphism A, C &
        K ** fi = G holds H = K by A11;
        take H;
        thus thesis by A26,A27;
      end;
      let a, b be set such that
A28:  a in dom (H.i) and
A29:  b in dom (H.i) and
A30:  H.i.a = H.i.b;
A31:  dom (H.s) = (the Sorts of X()).s by FUNCT_2:def 1
        .= rng((psi()-hash).s) by A24,MSUALG_3:def 3;
      then consider t1 being set such that
A32:  t1 in dom (psi()-hash.s) and
A33:  psi()-hash.s.t1 = a by A28,FUNCT_1:def 3;
      consider t2 being set such that
A34:  t2 in dom (psi()-hash.s) and
A35:  psi()-hash.s.t2 = b by A29,A31,FUNCT_1:def 3;
      reconsider t1, t2 as Element of (the Sorts of TermAlg S()).s by A32,A34;
      set e = t1 '=' t2;
A36:  fi-hash.s.t1 = ((H.s)*(psi()-hash.s)).t1 by A20,MSUALG_3:2
        .= H.s.a by A33,FUNCT_2:15
        .= ((H.s)*(psi()-hash.s)).t2 by A30,A35,FUNCT_2:15
        .= fi-hash.s.t2 by A20,MSUALG_3:2;
      for B being non-empty MSAlgebra over S() st P[B] holds B |= t1 '='
      t2 from EqTerms(A36,A25);
      then
A37:  X() |= e by A1,A3;
      thus a = psi()-hash.s.(e`1) by A33
        .= psi()-hash.s.(e`2) by A21,A37,EQUATION:def 5
        .= b by A35;
    end;
  end;
  then H is "1-1" by MSUALG_3:1;
  then H is_monomorphism X(), A by A19,MSUALG_3:def 9;
  then
A38: X(), Image H are_isomorphic by MSUALG_9:16;
  P[Image H] by A5,A10;
  hence thesis by A4,A38,MSUALG_3:17;
end;

:: Let P[] be an abstract class of algebras. Then P[] is an equational class
:: if and only if P[] is variety.

::$N Birkhoff Variety Theorem
scheme
  Birkhoff { S() -> non empty non void ManySortedSign, P[set] } : ex E being
EqualSet of S() st for A being non-empty MSAlgebra over S() holds P[A] iff A |=
  E
provided
A1: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic &
P[A] holds P[B] and
A2: for A being non-empty MSAlgebra over S() for B being strict
non-empty MSSubAlgebra of A st P[A] holds P[B] and
A3: for A being non-empty MSAlgebra over S(), R being MSCongruence of A
st P[A] holds P[QuotMSAlg (A,R)] and
A4: for I being set, F being MSAlgebra-Family of I, S() st (for i being
set st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product
F]
proof
A5: for A being non-empty MSAlgebra over S() for B being strict non-empty
  MSSubAlgebra of A st P[A] holds P[B] by A2;
  set XX = (the carrier of S()) --> NAT;
  set I = the carrier of S();
  defpred R[set,set] means ex s being SortSymbol of S() st $1 = s & $2 = {e
where e is Element of (Equations S()).s : for A being non-empty MSAlgebra over
  S() holds P[A] implies A |= e};
A6: now
    let w be set;
    assume w in I;
    then consider s being SortSymbol of S() such that
A7: s = w;
    take d = {e where e is Element of (Equations S()).s : for A being
    non-empty MSAlgebra over S() holds P[A] implies A |= e};
    thus R[w,d] by A7;
  end;
  consider E being ManySortedSet of I such that
A8: for i being set st i in I holds R[i,E.i] from PBOOLE:sch 3(A6);
  E is ManySortedSubset of Equations S()
  proof
    let j be set;
    assume j in I;
    then consider s being SortSymbol of S() such that
A9: j = s and
A10: E.j = {e where e is Element of (Equations S()).s : for A being
    non-empty MSAlgebra over S() holds P[A] implies A |= e} by A8;
    let q be set;
    assume q in E.j;
    then ex z being Element of (Equations S()).s st q = z & for A being
    non-empty MSAlgebra over S() holds P[A] implies A |= z by A10;
    hence thesis by A9;
  end;
  then reconsider E as EqualSet of S();
A11: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic & P[A
  ] holds P[B] by A1;
  defpred Q[MSAlgebra over S()] means $1 |= E;
A12: for D being non-empty MSAlgebra over S() holds Q[D] iff for s being
  SortSymbol of S(), e being Element of (Equations S()).s st (for M being
  non-empty MSAlgebra over S() st P[M] holds M |= e) holds D |= e
  proof
    let D be non-empty MSAlgebra over S();
    thus Q[D] implies for s being SortSymbol of S(), e being Element of (
Equations S()).s st (for B being non-empty MSAlgebra over S() st P[B] holds B
    |= e) holds D |= e
    proof
      assume
A13:  Q[D];
      let s be SortSymbol of S(), e be Element of (Equations S()).s such that
A14:  for B being non-empty MSAlgebra over S() st P[B] holds B |= e;
      R[s,E.s] by A8;
      then e in E.s by A14;
      hence thesis by A13,EQUATION:def 6;
    end;
    assume
A15: for s being SortSymbol of S(), e being Element of (Equations S())
.s st (for B being non-empty MSAlgebra over S() st P[B] holds B |= e) holds D
    |= e;
    let s be SortSymbol of S(), e be Element of (Equations S()).s such that
A16: e in E.s;
    R[s,E.s] by A8;
    then ex f being Element of (Equations S()).s st e = f & for A being
    non-empty MSAlgebra over S() holds P[A] implies A |= f by A16;
    hence thesis by A15;
  end;
A17: for A being non-empty MSAlgebra over S() for B being strict non-empty
  MSSubAlgebra of A holds Q[A] implies Q[B] by EQUATION:32;
A18: for I being set, F being MSAlgebra-Family of I, S() holds (for i being
  set st i in I ex A being MSAlgebra over S() st A = F.i & Q[A]) implies Q[
  product F] by EQUATION:38;
A19: for A, B being non-empty MSAlgebra over S() st A, B are_isomorphic
  holds Q[A] implies Q[B] by EQUATION:34;
  consider K being strict non-empty MSAlgebra over S(), F being
  ManySortedFunction of XX, the Sorts of K such that
A20: Q[K] and
A21: for B being non-empty MSAlgebra over S() for G being
ManySortedFunction of XX, the Sorts of B st Q[B] ex H being ManySortedFunction
of K, B st H is_homomorphism K, B & H ** F = G & for W being ManySortedFunction
of K, B st W is_homomorphism K, B & W ** F = G holds H = W from ExFreeAlg2(A19,
  A17,A18);
A22: for M being non-empty MSAlgebra over S() for G being ManySortedFunction
  of (the carrier of S()) --> NAT, the Sorts of M st Q[M] ex H being
  ManySortedFunction of K, M st H is_homomorphism K, M & G = H ** F
  proof
    let M be non-empty MSAlgebra over S(), G be ManySortedFunction of (the
    carrier of S()) --> NAT, the Sorts of M;
    assume Q[M];
    then ex H being ManySortedFunction of K, M st H is_homomorphism K, M & H
** F = G & for W being ManySortedFunction of K, M st W is_homomorphism K, M & W
    ** F = G holds H = W by A21;
    hence ex H being ManySortedFunction of K, M st H is_homomorphism K, M & H
    ** F = G;
  end;
A23: for I being set, F being MSAlgebra-Family of I, S() st (for i being set
  st i in I ex A being MSAlgebra over S() st A = F.i & P[A]) holds P[product F]
  by A4;
  take E;
  let A be non-empty MSAlgebra over S();
  hereby
    assume
A24: P[A];
    thus A |= E
    proof
      let s1 be SortSymbol of S();
A25:  R[s1,E.s1] by A8;
      let e be Element of (Equations S()).s1;
      assume e in E.s1;
      then consider x being Element of (Equations S()).s1 such that
A26:  e = x and
A27:  for A being non-empty MSAlgebra over S() holds P[A] implies A
      |= x by A25;
A28:  A |= x by A24,A27;
      let h be ManySortedFunction of TermAlg S(), A;
      assume h is_homomorphism TermAlg S(), A;
      hence thesis by A26,A28,EQUATION:def 5;
    end;
  end;
  assume
A29: A |= E;
A30: for A being non-empty MSAlgebra over S(), R being MSCongruence of A st P
  [A] holds P[QuotMSAlg (A,R)] by A3;
A31: Q[K] by A20;
A32: P[K] from FreeInModIsInVar(A12,A21,A31,A11,A5,A23);
A33: for B being strict non-empty finitely-generated MSSubAlgebra of A holds
  P[B]
  proof
    let B be strict non-empty finitely-generated MSSubAlgebra of A;
A34: Q[B] by A29,EQUATION:32;
    thus P[B] from FinGenAlgInVar(A34,A32,A22,A11,A30);
  end;
  thus P[A] from AllFinGen(A33,A11,A5,A30,A23);
end;