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

environ

 vocabularies XBOOLE_0, PBOOLE, STRUCT_0, MSUALG_1, SUBSET_1, PRALG_2, EQREL_1,
      FUNCT_1, CARD_3, RELAT_1, SETFAM_1, RLVECT_2, FUNCT_6, TARSKI, FUNCT_2,
      MARGREL1, UNIALG_2, FUNCT_5, FUNCOP_1, FINSEQ_4, PARTFUN1, MSUALG_3,
      MEMBER_1, ARYTM_3, WELLORD1, PRALG_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, STRUCT_0, FUNCT_2, FUNCOP_1, EQREL_1, FUNCT_5, FUNCT_6, CARD_3,
      PBOOLE, MSUALG_1, MSUALG_3, PRALG_2, PRALG_1, MSUALG_2;
 constructors EQREL_1, PRALG_1, PRALG_2, MSUALG_3, RELSET_1, FUNCT_5;
 registrations XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCOP_1, EQREL_1, PBOOLE, STRUCT_0, MSUALG_1, PRALG_2, MSUALG_3, CARD_3,
      RELSET_1;
 requirements BOOLE, SUBSET;
 definitions XBOOLE_0, FUNCT_1, MSUALG_3, PRALG_2, PBOOLE, TARSKI;
 theorems PBOOLE, FUNCT_1, EQREL_1, PRALG_2, MSUALG_1, MSUALG_3, FUNCT_2,
      CARD_3, TARSKI, FUNCOP_1, MSUALG_2, PRALG_1, FUNCT_6, RELAT_1, RELSET_1,
      XBOOLE_0, XBOOLE_1, PARTFUN1;
 schemes PBOOLE, MSSUBFAM;

begin  ::Preliminaries
::-------------------------------------------------------------------
:: Acknowledgements:
:: ================
::
:: I would like to thank Professor A.Trybulec for his help in the preparation
:: of the article.
::-------------------------------------------------------------------

reserve I for non empty set,
  J for ManySortedSet of I,
  S for non void non empty ManySortedSign,
  i for Element of I,
  c for set,
  A for MSAlgebra-Family of I,S,
  EqR for Equivalence_Relation of I,
  U0,U1,U2 for MSAlgebra over S,
  s for SortSymbol of S,
  o for OperSymbol of S,
  f for Function;

registration
  let I be set, S;
  let AF be MSAlgebra-Family of I,S;
  cluster product AF -> non-empty;
  coherence by MSUALG_1:def 3;
end;

registration
  let X be with_non-empty_elements set;
  cluster id X -> non-empty;
  coherence
  proof
    reconsider NE = id X as ManySortedSet of X;
    NE is non-empty
    proof
      let i be set;
      assume i in X;
      hence thesis by FUNCT_1:17;
    end;
    hence thesis;
  end;
end;

theorem Th1:
  for f,F being Function, A being set st f in product F holds f|A
  in product(F|A)
proof
  let f,F be Function, A be set;
  assume
A1: f in product F;
  then dom f = dom F by CARD_3:9;
  then
A2: dom (f|A) = dom F /\ A by RELAT_1:61
    .= dom (F|A)by RELAT_1:61;
  for x be set st x in dom (F|A) holds (f|A).x in (F|A).x
  proof
    let x be set;
    assume
A3: x in dom (F|A);
    then x in dom F /\ A by RELAT_1:61;
    then
A4: x in dom F by XBOOLE_0:def 4;
    (F|A).x = F.x & (f|A).x = f.x by A2,A3,FUNCT_1:47;
    hence thesis by A1,A4,CARD_3:9;
  end;
  hence thesis by A2,CARD_3:9;
end;

theorem Th2:
  for A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non
empty Subset of I, Aa be MSAlgebra-Family of a,S st A|a = Aa holds Carrier(Aa,s
  ) = (Carrier(A,s))|a
proof
  let A be MSAlgebra-Family of I,S, s be SortSymbol of S, a be non empty
  Subset of I, Aa be MSAlgebra-Family of a,S such that
A1: A|a = Aa;
  dom ((Carrier(A,s))|a) = dom (Carrier(A,s)) /\ a by RELAT_1:61
    .= I /\ a by PARTFUN1:def 2
    .= a by XBOOLE_1:28;
  then reconsider Cas = ((Carrier(A,s))|a) as ManySortedSet of a by
PARTFUN1:def 2;
  for i be set st i in a holds (Carrier(Aa,s)).i = Cas.i
  proof
    let i be set;
    assume
A2: i in a;
    then reconsider i9 = i as Element of a;
    reconsider i99 = i9 as Element of I;
A3: Aa.i9 = A.i9 & ex U1 being MSAlgebra over S st U1 = A.i99 & (Carrier(A
    ,s) ).i99 = (the Sorts of U1).s by A1,FUNCT_1:49,PRALG_2:def 9;
    ex U0 being MSAlgebra over S st U0 = Aa.i & (Carrier(Aa,s) ).i = (the
    Sorts of U0).s by A2,PRALG_2:def 9;
    hence thesis by A3,FUNCT_1:49;
  end;
  hence thesis by PBOOLE:3;
end;

theorem Th3:
  for i be set, I be non empty set, EqR be Equivalence_Relation of
  I, c1,c2 be Element of Class EqR st i in c1 & i in c2 holds c1 = c2
proof
  let i be set, I be non empty set, EqR be Equivalence_Relation of I, c1,c2 be
  Element of Class EqR such that
A1: i in c1 and
A2: i in c2;
  consider x1 be set such that
  x1 in I and
A3: c1 = Class(EqR,x1) by EQREL_1:def 3;
A4: [i,x1] in EqR by A1,A3,EQREL_1:19;
  consider x2 be set such that
  x2 in I and
A5: c2 = Class(EqR,x2) by EQREL_1:def 3;
  [i,x2] in EqR by A2,A5,EQREL_1:19;
  then Class(EqR,x2) = Class(EqR,i) by A1,EQREL_1:35
    .= c1 by A1,A3,A4,EQREL_1:35;
  hence thesis by A5;
end;

Lm1: for f be Function, x be set st x in product f holds x is Function;

theorem
  for D being non empty set for F being ManySortedFunction of D for C
  being with_common_domain functional non empty set st C = rng F for d being
  Element of D,e being set st e in DOM C holds F.d.e = (commute F).e.d
proof
  let D be non empty set;
  let F be ManySortedFunction of D;
  set E = union { rng(F.d9) where d9 is Element of D : not contradiction};
  reconsider F9= F as Function;
  let C be with_common_domain functional non empty set such that
A1: C = rng F;
A2: rng F9 c= Funcs(DOM C,E)
  proof
    let x be set;
    assume x in rng F9;
    then consider d9 be set such that
A3: d9 in dom F and
A4: F.d9 = x by FUNCT_1:def 3;
    reconsider d9 as Element of D by A3;
    consider Fd be Function such that
A5: Fd = F.d9;
A6: rng Fd c= E
    proof
A7:   rng Fd in { rng(F.d99) where d99 is Element of D : not
      contradiction} by A5;
      let x1 be set;
      assume x1 in rng Fd;
      hence thesis by A7,TARSKI:def 4;
    end;
    F.d9 in rng F by A3,FUNCT_1:def 3;
    then dom Fd = DOM C by A1,A5,CARD_3:108;
    hence thesis by A4,A5,A6,FUNCT_2:def 2;
  end;
  let d be Element of D,e be set;
  assume
A8: e in DOM C;
  dom F9 = D by PARTFUN1:def 2;
  then F in Funcs(D,Funcs(DOM C,E)) by A2,FUNCT_2:def 2;
  hence thesis by A8,FUNCT_6:56;
end;

begin  :: Constants of Many Sorted Algebras

definition
  let S,U0;
  let o be OperSymbol of S;
  func const(o,U0) equals
  Den(o,U0).{};
  correctness;
end;

theorem Th5:
  the_arity_of o = {} & Result(o,U0) <> {} implies const(o,U0) in Result(o,U0)
proof
  assume that
A1: the_arity_of o = {} and
A2: Result(o,U0) <> {};
  dom Den(o,U0) = Args(o,U0) by A2,FUNCT_2:def 1
    .= {{}} by A1,PRALG_2:4;
  then {} in dom Den(o,U0) by TARSKI:def 1;
  then Den(o,U0).{} in rng Den(o,U0) by FUNCT_1:def 3;
  hence thesis;
end;

theorem
  (the Sorts of U0).s <> {} implies Constants(U0,s) = { const(o,U0)
  where o is Element of the carrier' of S : the_result_sort_of o = s &
  the_arity_of o = {} }
proof
  assume
A1: (the Sorts of U0).s <> {};
  thus Constants(U0,s) c= { const(o,U0) where o is Element of the carrier' of
S: the_result_sort_of o = s & the_arity_of o = {} }
  proof
    let x be set;
    assume
A2: x in Constants(U0,s);
    ex A being non empty set st A =(the Sorts of U0).s & Constants(U0,s) =
{ a where a is Element of A : ex o be OperSymbol of S st (the Arity of S).o =
{} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A1,MSUALG_2:def 3;
    then consider A being non empty set such that
    A =(the Sorts of U0).s and
A3: x in { a where a is Element of A : ex o be OperSymbol of S st (the
Arity of S).o = {} & (the ResultSort of S).o = s & a in rng Den(o,U0)} by A2;
    consider a be Element of A such that
A4: a = x and
A5: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
    ResultSort of S).o = s & a in rng Den(o,U0) by A3;
    consider o1 be OperSymbol of S such that
A6: (the Arity of S).o1 = {} and
A7: (the ResultSort of S).o1 = s and
A8: a in rng Den(o1,U0) by A5;
A9: ex x1 be set st x1 in dom Den(o1,U0) & a = Den(o1,U0).x1 by A8,
FUNCT_1:def 3;
A10: the_result_sort_of o1 = s by A7,MSUALG_1:def 2;
A11: the_arity_of o1 = {} by A6,MSUALG_1:def 1;
    then Args(o1,U0) = {{}} by PRALG_2:4;
    then x = const(o1,U0) by A4,A9,TARSKI:def 1;
    hence thesis by A10,A11;
  end;
  let x be set;
  assume x in { const(o,U0) where o is Element of the carrier' of S :
  the_result_sort_of o = s & the_arity_of o = {} };
  then consider o being Element of the carrier' of S such that
A12: x = const(o,U0) and
A13: the_result_sort_of o = s and
A14: the_arity_of o = {};
  o in the carrier' of S;
  then
A15: o in dom (the ResultSort of S) by FUNCT_2:def 1;
A16: Result(o,U0) = ((the Sorts of U0) * the ResultSort of S).o by
MSUALG_1:def 5
    .= (the Sorts of U0).((the ResultSort of S).o) by A15,FUNCT_1:13
    .= (the Sorts of U0).s by A13,MSUALG_1:def 2;
  thus x in Constants(U0,s)
  proof
A17: ex o be OperSymbol of S st (the Arity of S).o = {} & (the ResultSort
    of S).o = s & x in rng Den(o,U0)
    proof
      take o;
      Args(o,U0) = dom Den(o,U0) & Args(o,U0) = {{}} by A1,A14,A16,
FUNCT_2:def 1,PRALG_2:4;
      then {} in dom Den(o,U0) by TARSKI:def 1;
      hence thesis by A12,A13,A14,FUNCT_1:def 3,MSUALG_1:def 1,def 2;
    end;
    consider A being non empty set such that
A18: A =(the Sorts of U0).s and
A19: Constants(U0,s) = { a where a is Element of A : ex o be
OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = s & a in
    rng Den(o,U0)} by A1,MSUALG_2:def 3;
    x is Element of A by A12,A14,A16,A18,Th5;
    hence thesis by A19,A17;
  end;
end;

theorem Th7:
  the_arity_of o = {} implies (commute (OPER A)).o in Funcs(I,Funcs
  ({{}}, union { Result(o,A.i9) where i9 is Element of I: not contradiction }))
proof
  set f = (commute (OPER A)).o;
  set C = union { Result(o,A.i9) where i9 is Element of I: not contradiction };
  commute (OPER A) in Funcs(the carrier' of S, Funcs(I,rng uncurry (OPER A
  ))) by PRALG_2:6;
  then
A1: ex f1 be Function st commute (OPER A) = f1 & dom f1 = the carrier' of S &
  rng f1 c= Funcs(I,rng uncurry (OPER A)) by FUNCT_2:def 2;
  then f in rng commute (OPER A) by FUNCT_1:def 3;
  then
A2: ex fb be Function st fb = f & dom fb = I & rng fb c= rng uncurry (OPER A)
  by A1,FUNCT_2:def 2;
  assume
A3: the_arity_of o = {};
  now
    let x be set;
    assume x in rng f;
    then consider a be set such that
A4: a in dom f and
A5: f.a = x by FUNCT_1:def 3;
    f = A?.o;
    then reconsider x9 = x as Function by A5;
    reconsider a as Element of I by A2,A4;
A6: x9 = (A?.o).a by A5
      .= Den(o,A.a) by PRALG_2:7;
    then
A7: dom x9 = Args(o,A.a) by FUNCT_2:def 1
      .= {{}} by A3,PRALG_2:4;
    now
      let c be set;
      assume c in rng x9;
      then consider b be set such that
A8:   b in dom x9 and
A9:   x9.b = c by FUNCT_1:def 3;
      x9.b = const(o,A.a) by A6,A7,A8,TARSKI:def 1;
      then
A10:  c is Element of Result(o,A.a) by A3,A9,Th5;
      Result(o,A.a) in { Result(o,A.i9) where i9 is Element of I: not
      contradiction };
      hence c in C by A10,TARSKI:def 4;
    end;
    then rng x9 c= C by TARSKI:def 3;
    hence x in Funcs({{}},C) by A7,FUNCT_2:def 2;
  end;
  then rng f c= Funcs({{}},C) by TARSKI:def 3;
  hence thesis by A2,FUNCT_2:def 2;
end;

theorem Th8:
  the_arity_of o = {} implies const(o,product A) in Funcs(I, union
  { Result(o,A.i9) where i9 is Element of I: not contradiction })
proof
  set g = (commute (OPER A)).o;
  set C = union { Result(o,A.i9) where i9 is Element of I: not contradiction };
  assume
A1: the_arity_of o = {};
  then
A2: g in Funcs(I,Funcs({{}},C)) by Th7;
  reconsider g as Function;
  (OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)))
  by PRALG_2:def 13
    .= commute(A?.o) by A1,FUNCOP_1:def 8;
  then
A3: const(o,product A) = (commute g).{} by MSUALG_1:def 6;
  commute g in Funcs({{}},Funcs(I,C)) by A2,FUNCT_6:55;
  then consider g1 be Function such that
A4: g1 = commute g and
A5: dom g1 = {{}} and
A6: rng g1 c= Funcs(I,C) by FUNCT_2:def 2;
  {} in {{}} by TARSKI:def 1;
  then g1.{} in rng g1 by A5,FUNCT_1:def 3;
  hence thesis by A3,A4,A6;
end;

registration
  let S,I,o,A;
  cluster const (o,product A) -> Relation-like Function-like;
  coherence
  proof
    const(o,product A) is Function
    proof
      per cases;
      suppose
        the_arity_of o = {};
        then
        const(o,product A) in Funcs(I, union { Result(o,A.i9) where i9 is
        Element of I: not contradiction }) by Th8;
        then ex g be Function st g = const(o,product A) & dom g = I & rng g c=
        union { Result(o,A.i9) where i9 is Element of I: not contradiction }
by FUNCT_2:def 2;
        hence thesis;
      end;
      suppose
A1:     the_arity_of o <> {};
        dom ((the Sorts of (product A))*(the_arity_of o)) = dom (
        the_arity_of o ) by PRALG_2:3;
        then
A2:     dom ((the Sorts of (product A))*(the_arity_of o)) <> dom {} by A1;
        dom Den(o,product A) = Args(o,product A) by FUNCT_2:def 1
          .= product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3
;
        then not {} in dom Den(o,product A) by A2,CARD_3:9;
        hence thesis by FUNCT_1:def 2;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th9:
  for o be OperSymbol of S st the_arity_of o = {} holds (const (o,
  product A)).i = const (o,A.i)
proof

  let o be OperSymbol of S such that
A1: the_arity_of o = {};
  set f = (commute (OPER A)).o, C = union { Result(o,A.i9) where i9 is Element
  of I: not contradiction };
A2: f in Funcs(I,Funcs({{}},C)) by A1,Th7;
  (OPS A).o = (IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)))
  by PRALG_2:def 13
    .= commute(A?.o) by A1,FUNCOP_1:def 8;
  then
A3: const(o,product A) = (commute f).{} by MSUALG_1:def 6;
A4: {} in {{}} by TARSKI:def 1;
  const (o,A.i) = ((A?.o).i).{} by PRALG_2:7
    .= const(o,product A).i by A2,A3,A4,FUNCT_6:56;
  hence thesis;
end;

theorem
  the_arity_of o = {} & dom f = I & (for i be Element of I holds f.i =
  const(o,A.i)) implies f = const(o,product A)
proof
  assume that
A1: the_arity_of o = {} and
A2: dom f = I and
A3: for i be Element of I holds f.i = const(o,A.i);
A4: now
    let a be set;
    assume a in I;
    then reconsider a9 = a as Element of I;
    thus f.a = const(o,A.a9) by A3
      .= (const(o,product A)).a by A1,Th9;
  end;
  set C = union { Result(o,A.i9) where i9 is Element of I: not contradiction };
  const(o,product A) in Funcs(I,C) by A1,Th8;
  then ex g2 be Function st g2 = const(o,product A) & dom g2 = I & rng g2 c= C
  by FUNCT_2:def 2;
  hence thesis by A2,A4,FUNCT_1:2;
end;

theorem Th11:
  for e be Element of Args(o,U1) st e = {} & the_arity_of o = {} &
Args(o,U1) <> {} & Args(o,U2) <> {} for F be ManySortedFunction of U1,U2 holds
  F#e = {}
proof
  let e be Element of Args(o,U1) such that
A1: e = {} and
A2: the_arity_of o = {} and
A3: Args(o,U1) <> {} & Args(o,U2) <> {};
  reconsider e1 = e as Function by A1;
  let F be ManySortedFunction of U1,U2;
  rng (the_arity_of o) = {} by A2;
  then rng (the_arity_of o) c= dom F by XBOOLE_1:2;
  then
A4: dom (F*the_arity_of o) = dom (the_arity_of o) by RELAT_1:27
    .= {} by A2;
  then rng (F*the_arity_of o) = {} by RELAT_1:42;
  then (F*the_arity_of o) is Function of {},{} by A4,FUNCT_2:1;
  then
A5: e1 in product (doms (F*the_arity_of o)) by A1,CARD_3:10,FUNCT_6:23
,TARSKI:def 1;
A6: F#e = (Frege(F*the_arity_of o)).e by A3,MSUALG_3:def 5
    .= (F*the_arity_of o)..e1 by A5,PRALG_2:def 2;
  then reconsider fn = F#e as Function;
A7: dom fn = {} by A4,A6,PRALG_1:def 17;
  thus thesis by A7;
end;

begin :: Properties of Arguments of operations in Many Sorted Algebras

theorem Th12:
  for U1,U2 be non-empty MSAlgebra over S for F be
  ManySortedFunction of U1,U2 for x be Element of Args(o,U1) holds x in product
  doms (F*the_arity_of o)
proof
  let U1,U2 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  let x be Element of Args(o,U1);
  x in Args(o,U1);
  then
A1: x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
  then
A2: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by CARD_3:9
    .= dom (the_arity_of o) by PRALG_2:3;
  dom F = (the carrier of S) by PARTFUN1:def 2;
  then
A3: rng (the_arity_of o) c= dom F;
A4: now
    let n be set;
    assume n in dom (doms (F*the_arity_of o));
    then n in (F*the_arity_of o)"SubFuncs rng (F*the_arity_of o) by
FUNCT_6:def 2;
    then n in dom (F*the_arity_of o) by FUNCT_6:19;
    hence n in dom x by A3,A2,RELAT_1:27;
  end;
A5: dom x = dom ((the Sorts of U1)*(the_arity_of o)) by A1,CARD_3:9;
A6: now
    let n be set;
    assume
A7: n in dom (doms (F*the_arity_of o));
    then
A8: n in dom (the_arity_of o) by A2,A4;
    then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
    then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S);
A9: n in dom (F*the_arity_of o) by A3,A8,RELAT_1:27;
    then (F*the_arity_of o).n = F.s1 by FUNCT_1:12;
    then
A10: (doms (F*the_arity_of o)).n = dom (F.s1) by A9,FUNCT_6:22
      .= (the Sorts of U1).s1 by FUNCT_2:def 1;
    n in dom ((the Sorts of U1)*(the_arity_of o)) by A5,A4,A7;
    then x.n in ((the Sorts of U1)*(the_arity_of o)).n by A1,CARD_3:9;
    hence x.n in (doms (F*the_arity_of o)).n by A5,A4,A7,A10,FUNCT_1:12;
  end;
  now
    let n be set;
    assume n in dom x;
    then
A11: n in dom (F*the_arity_of o) by A3,A2,RELAT_1:27;
    (F*the_arity_of o).n is Function;
    then n in (F*the_arity_of o)"SubFuncs rng (F*the_arity_of o) by A11,
FUNCT_6:19;
    hence n in dom (doms (F*the_arity_of o)) by FUNCT_6:def 2;
  end;
  then
A12: dom x c= dom (doms (F*the_arity_of o)) by TARSKI:def 3;
  dom (doms (F*the_arity_of o)) c= dom x by A4,TARSKI:def 3;
  then dom x = dom (doms (F*the_arity_of o)) by A12,XBOOLE_0:def 10;
  hence thesis by A6,CARD_3:9;
end;

theorem Th13:
  for U1,U2 be non-empty MSAlgebra over S for F be
ManySortedFunction of U1,U2 for x be Element of Args(o,U1) for n be set st n in
  dom (the_arity_of o) holds (F#x).n = F.((the_arity_of o)/.n).(x.n)
proof
  let U1,U2 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of U1,U2;
  let x be Element of Args(o,U1);
  let n be set such that
A1: n in dom (the_arity_of o);
  dom F = (the carrier of S) by PARTFUN1:def 2;
  then rng (the_arity_of o) c= dom F;
  then
A2: n in dom (F*the_arity_of o) by A1,RELAT_1:27;
A3: x in product doms (F*the_arity_of o) by Th12;
  thus (F#x).n = ((Frege(F*the_arity_of o)).x).n by MSUALG_3:def 5
    .= ((F*the_arity_of o)..x).n by A3,PRALG_2:def 2
    .= ((F*the_arity_of o).n).(x.n) by A2,PRALG_1:def 17
    .= (F.((the_arity_of o).n)).(x.n) by A2,FUNCT_1:12
    .= F.((the_arity_of o)/.n).(x.n) by A1,PARTFUN1:def 6;
end;

theorem Th14:
  for x be Element of Args(o,product A) holds x in Funcs (dom (
the_arity_of o),Funcs (I,union { (the Sorts of A.i9).s9 where i9 is Element of
  I,s9 is Element of (the carrier of S) : not contradiction }))
proof
  let x be Element of Args(o,product A);
  set C = union { (the Sorts of A.i9).s9 where i9 is Element of I, s9 is
  Element of (the carrier of S) : not contradiction };
  consider x1 be Function such that
A1: x1 = x;
  x in Args(o,product A);
  then
A2: x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
  dom (SORTS A) = the carrier of S by PARTFUN1:def 2;
  then
A3: rng (the_arity_of o) c= dom (SORTS A);
  now
    let c be set;
    assume c in rng x1;
    then consider n be set such that
A4: n in dom x1 and
A5: x1.n = c by FUNCT_1:def 3;
A6: n in dom ((SORTS A)*(the_arity_of o)) by A2,A1,A4,CARD_3:9;
    then n in dom (the_arity_of o) by A3,RELAT_1:27;
    then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
    then reconsider s1 = (the_arity_of o).n as Element of (the carrier of S);
    x1.n in ((SORTS A)*(the_arity_of o)).n by A2,A1,A6,CARD_3:9;
    then x1.n in (SORTS A).s1 by A6,FUNCT_1:12;
    then x1.n in product Carrier(A,s1) by PRALG_2:def 10;
    then consider g be Function such that
A7: g = x1.n and
A8: dom g = dom Carrier(A,s1) and
A9: for i9 be set st i9 in dom (Carrier(A,s1)) holds g.i9 in (Carrier
    (A,s1)).i9 by CARD_3:def 5;
    now
      let c1 be set;
      assume c1 in rng g;
      then consider i1 be set such that
A10:  i1 in dom g and
A11:  g.i1 = c1 by FUNCT_1:def 3;
      reconsider i1 as Element of I by A8,A10;
      ex U0 being MSAlgebra over S st U0 = A.i1 & (Carrier(A,s1 )).i1 = (
      the Sorts of U0).s1 by PRALG_2:def 9;
      then
A12:  g.i1 in (the Sorts of A.i1).s1 by A8,A9,A10;
      (the Sorts of A.i1).s1 in {(the Sorts of A.i9).s9 where i9 is
      Element of I, s9 is Element of (the carrier of S) : not contradiction };
      hence c1 in C by A11,A12,TARSKI:def 4;
    end;
    then
A13: rng g c= C by TARSKI:def 3;
    dom g = I by A8,PARTFUN1:def 2;
    hence c in Funcs(I,C) by A5,A7,A13,FUNCT_2:def 2;
  end;
  then
A14: rng x1 c= Funcs(I,C) by TARSKI:def 3;
  dom x = dom ((SORTS A)*(the_arity_of o)) by A2,CARD_3:9
    .= dom (the_arity_of o) by A3,RELAT_1:27;
  hence thesis by A1,A14,FUNCT_2:def 2;
end;

theorem Th15:
  for x be Element of Args(o,product A) for n be set st n in dom (
  the_arity_of o) holds x.n in product Carrier(A,(the_arity_of o)/.n)
proof
  let x be Element of Args(o,product A);
  let n be set such that
A1: n in dom (the_arity_of o);
  dom (SORTS A) = the carrier of S by PARTFUN1:def 2;
  then rng (the_arity_of o) c= dom (SORTS A);
  then
A2: n in dom ((SORTS A)*(the_arity_of o)) by A1,RELAT_1:27;
  x in Args(o,product A);
  then x in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3
;
  then x.n in ((SORTS A)*(the_arity_of o)).n by A2,CARD_3:9;
  then x.n in (SORTS A).((the_arity_of o).n) by A2,FUNCT_1:12;
  then x.n in (SORTS A).((the_arity_of o)/.n) by A1,PARTFUN1:def 6;
  hence thesis by PRALG_2:def 10;
end;

theorem Th16:
  for i be Element of I for n be set st n in dom(the_arity_of o)
for s be SortSymbol of S st s = (the_arity_of o).n for y be Element of Args(o,
  product A) for g be Function st g = y.n holds g.i in (the Sorts of A.i).s
proof
  let i be Element of I;
  let n be set;
  assume n in dom(the_arity_of o);
  then
A1: n in dom ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
  let s be SortSymbol of S such that
A2: s = (the_arity_of o).n;
  let y be Element of Args(o,product A);
  y in Args(o,product A);
  then
A3: y in product ((the Sorts of (product A))*(the_arity_of o)) by PRALG_2:3;
  let g be Function;
  assume g = y.n;
  then g in ((the Sorts of (product A))*(the_arity_of o)).n by A1,A3,CARD_3:9;
  then g in (the Sorts of (product A)).s by A2,A1,FUNCT_1:12;
  then
A4: g in product Carrier(A,s) by PRALG_2:def 10;
  i in I;
  then
A5: i in dom (Carrier(A,s)) by PARTFUN1:def 2;
  ex U0 being MSAlgebra over S st U0 = A.i & (Carrier(A,s)) .i = (the
  Sorts of U0).s by PRALG_2:def 9;
  hence thesis by A5,A4,CARD_3:9;
end;

theorem Th17:
  for y be Element of Args(o,product A) st (the_arity_of o) <> {}
  holds (commute y) in product doms (A?.o)
proof
  let y be Element of Args(o,product A);
  set D = union { (the Sorts of A.i9).s9 where i9 is Element of I,s9 is
  Element of (the carrier of S) : not contradiction };
A1: y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
  assume (the_arity_of o) <> {};
  then commute y in Funcs (I,Funcs (dom (the_arity_of o),D)) by A1,FUNCT_6:55;
  then
A2: ex f be Function st f = commute y & dom f = I & rng f c= Funcs (dom (
  the_arity_of o),D) by FUNCT_2:def 2;
A3: now
    let i1 be set;
    assume i1 in dom (doms (A?.o));
    then reconsider ii =i1 as Element of I by PRALG_2:11;
A4: now
      let n be set;
      assume
A5:   n in dom ((the Sorts of A.ii)*(the_arity_of o));
      then
A6:   n in dom (the_arity_of o) by PRALG_2:3;
      then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
      then reconsider s1 = (the_arity_of o).n as SortSymbol of S;
A7:   ex ff be Function st ff = y & dom ff = dom (the_arity_of o) & rng ff
      c= Funcs(I,D) by A1,FUNCT_2:def 2;
      then n in dom y by A5,PRALG_2:3;
      then y.n in rng y by FUNCT_1:def 3;
      then consider g be Function such that
A8:   g = y.n and
      dom g = I and
      rng g c= D by A7,FUNCT_2:def 2;
      ((commute y).ii).n = g.ii & g.ii in (the Sorts of A.ii).s1 by A1,A6,A8
,Th16,FUNCT_6:56;
      hence ((commute y).ii).n in ((the Sorts of A.ii)*(the_arity_of o)).n by
A5,FUNCT_1:12;
    end;
    (commute y).ii in rng (commute y) by A2,FUNCT_1:def 3;
    then
    ex h be Function st h = (commute y).ii & dom h = dom ( the_arity_of o)
    & rng h c= D by A2,FUNCT_2:def 2;
    then dom((commute y).ii) = dom ((the Sorts of A.ii)*(the_arity_of o)) by
PRALG_2:3;
    then (commute y).ii in product ((the Sorts of A.ii)*(the_arity_of o)) by A4
,CARD_3:9;
    then (commute y).ii in Args(o,A.ii) by PRALG_2:3;
    hence (commute y).i1 in (doms (A?.o)).i1 by PRALG_2:11;
  end;
  dom (commute y) = dom (doms (A?.o)) by A2,PRALG_2:11;
  hence thesis by A3,CARD_3:9;
end;

theorem Th18:
  for y be Element of Args(o,product A) st the_arity_of o <> {}
  holds y in dom (Commute Frege(A?.o))
proof
  let y be Element of Args(o,product A);
  set D = union { (the Sorts of A.ii).ss where ii is Element of I,ss is
  Element of (the carrier of S) : not contradiction };
  assume
A1: the_arity_of o <> {};
  then (commute y) in product doms (A?.o) by Th17;
  then
A2: (commute y) in dom (Frege(A?.o)) by PARTFUN1:def 2;
  y in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
  then y = commute commute y by A1,FUNCT_6:57;
  hence thesis by A2,PRALG_2:def 1;
end;

theorem Th19:
  for I be set, S be non void non empty ManySortedSign, A be
  MSAlgebra-Family of I,S, o be OperSymbol of S for x be Element of Args(o,
product A) holds Den(o,product A).x in product Carrier(A,the_result_sort_of o)
proof
  let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family
  of I,S, o be OperSymbol of S;
  let x be Element of Args(o,product A);
  Result(o,product A) = (SORTS A).(the_result_sort_of o) by PRALG_2:3
    .= product Carrier(A,the_result_sort_of o) by PRALG_2:def 10;
  hence thesis;
end;

theorem Th20:
  for I,S,A,i for o be OperSymbol of S st (the_arity_of o) <> {}
  for U1 be non-empty MSAlgebra over S for x be Element of Args(o,product A)
  holds (commute x).i is Element of Args(o,A.i)
proof
  let I,S,A,i;
  let o be OperSymbol of S such that
A1: (the_arity_of o) <> {};
  let U1 be non-empty MSAlgebra over S;
  let x be Element of Args(o,product A);
  i in I;
  then
A2: i in dom (doms(A?.o)) by PRALG_2:11;
  (commute x) in product doms(A?.o) by A1,Th17;
  then (commute x).i in doms(A?.o).i by A2,CARD_3:9;
  hence thesis by PRALG_2:11;
end;

theorem Th21:
  for I,S,A,i,o for x be Element of Args(o,product A) for n be set
st n in dom(the_arity_of o) for f be Function st f = x.n holds ((commute x).i).
  n = f.i
proof
  let I,S,A,i,o;
  let x be Element of Args(o,product A);
  let n be set such that
A1: n in dom(the_arity_of o);
  set C = union { (the Sorts of A.i9).s9 where i9 is Element of I,s9 is
  Element of (the carrier of S) : not contradiction };
A2: x in Funcs (dom (the_arity_of o),Funcs (I,C)) by Th14;
  let g be Function;
  assume g = x.n;
  hence thesis by A1,A2,FUNCT_6:56;
end;

theorem Th22:
  for o be OperSymbol of S st (the_arity_of o) <> {} for y be
Element of Args(o,product A), i9 be Element of I for g be Function st g = Den(o
  ,product A).y holds g.i9 = Den(o,A.i9).((commute y).i9)
proof
  let o be OperSymbol of S such that
A1: (the_arity_of o) <> {};
  let y be Element of Args(o,product A), i9 be Element of I;
A2: y in dom (Commute Frege(A?.o)) by A1,Th18;
A3: (commute y) in product doms (A?.o) by A1,Th17;
A4: Den(o,product A) = (OPS A).o by MSUALG_1:def 6
    .= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by
PRALG_2:def 13
    .= (Commute Frege(A?.o)) by A1,FUNCOP_1:def 8;
A5: dom (A?.o) = I by PARTFUN1:def 2;
  let g be Function;
  assume g = Den(o,product A).y;
  then g = (Frege(A?.o)).(commute y) by A4,A2,PRALG_2:def 1
    .= (A?.o)..(commute y) by A3,PRALG_2:def 2;
  then g.i9 = ((A?.o).i9).((commute y).i9) by A5,PRALG_1:def 17
    .= Den(o,A.i9).((commute y).i9) by PRALG_2:7;
  hence thesis;
end;

begin :: The Projection of Family of Many Sorted Algebras

definition
  let I,S;

  let A be MSAlgebra-Family of I,S, i be Element of I;
  func proj(A,i) -> ManySortedFunction of product A,A.i means
  :Def2:
  for s be Element of S holds it.s = proj (Carrier(A,s), i);
  existence
  proof
    deffunc G(Element of S) = proj (Carrier(A,$1), i);
    consider F be ManySortedSet of the carrier of S such that
A1: for s be Element of S holds F.s = G(s) from PBOOLE:sch 5;
    F is ManySortedFunction of product A,A.i
    proof
      let s be set such that
A2:   s in the carrier of S;
      F.s is Function of (the Sorts of product A).s, (the Sorts of A.i).s
      proof
        reconsider s9 = s as Element of S by A2;
        F.s = proj (Carrier(A,s9),i) by A1;
        then reconsider F9 = F.s as Function;
A3:     rng F9 c= (the Sorts of A.i).s
        proof
          let y be set;
A4:       dom (Carrier(A,s9)) = I & ex U0 being MSAlgebra over S st U0 =
A.i & ( Carrier(A,s9) ).i = (the Sorts of U0).s9 by PARTFUN1:def 2
,PRALG_2:def 9;
          assume y in rng F9;
          then y in rng (proj (Carrier(A,s9),i)) by A1;
          then consider x1 be set such that
A5:       x1 in dom (proj (Carrier(A,s9),i)) and
A6:       y = (proj (Carrier(A,s9),i)).x1 by FUNCT_1:def 3;
A7:       x1 in product (Carrier(A,s9)) by A5;
          then reconsider x1 as Function;
          y = x1.i by A5,A6,CARD_3:def 16;
          hence thesis by A7,A4,CARD_3:9;
        end;
        dom F9 = dom (proj (Carrier(A,s9),i)) by A1
          .= product (Carrier(A,s9)) by CARD_3:def 16
          .= (the Sorts of product A).s by PRALG_2:def 10;
        hence thesis by A2,A3,FUNCT_2:def 1,RELSET_1:4;
      end;
      hence thesis;
    end;
    then reconsider F9 = F as ManySortedFunction of product A,A.i;
    take F9;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F,G be ManySortedFunction of product A,A.i such that
A8: for s be Element of S holds F.s = proj (Carrier(A,s), i) and
A9: for s be Element of S holds G.s = proj (Carrier(A,s), i);
    now
      let s9 be set;
      assume s9 in (the carrier of S);
      then reconsider s99 = s9 as Element of S;
      thus F.s9 = proj (Carrier(A,s99), i) by A8
        .= G.s9 by A9;
    end;
    hence F = G by PBOOLE:3;
  end;
end;

theorem Th23:
  for x be Element of Args(o,product A) st the_arity_of o <> {}
  for i be Element of I holds proj(A,i)#x = (commute x).i
proof
  let x be Element of Args(o,product A) such that
A1: the_arity_of o <> {};
  set C = union { (the Sorts of A.i9).s9 where i9 is Element of I, s9 is
  Element of (the carrier of S) : not contradiction };
  let i be Element of I;
A2: x in Funcs (dom (the_arity_of o),Funcs(I,C)) by Th14;
  then
A3: commute x in Funcs(I,Funcs(dom (the_arity_of o),C)) by A1,FUNCT_6:55;
  then dom (commute x) = I by FUNCT_2:92;
  then
A4: (commute x).i in rng (commute x) by FUNCT_1:def 3;
A5: now
A6: rng x c= Funcs(I,C) by A2,FUNCT_2:92;
    let n be set such that
A7: n in dom (the_arity_of o);
    x.n in product Carrier(A,(the_arity_of o)/.n) by A7,Th15;
    then
A8: x.n in dom (proj (Carrier(A,(the_arity_of o)/.n),i)) by CARD_3:def 16;
    n in dom x by A2,A7,FUNCT_2:92;
    then x.n in rng x by FUNCT_1:def 3;
    then consider g be Function such that
A9: g = x.n and
    dom g = I and
    rng g c= C by A6,FUNCT_2:def 2;
    thus ((proj(A,i))#x).n = ((proj(A,i)).((the_arity_of o)/.n)).(x.n) by A7
,Th13
      .= (proj (Carrier(A,(the_arity_of o)/.n),i)).(x.n) by Def2
      .= g.i by A9,A8,CARD_3:def 16
      .= ((commute x).i).n by A2,A7,A9,FUNCT_6:56;
  end;
A10: x in product doms ((proj(A,i))*the_arity_of o) by Th12;
  rng (commute x) c= Funcs(dom (the_arity_of o), C) by A3,FUNCT_2:92;
  then
A11: dom ((commute x).i) = dom (the_arity_of o) by A4,FUNCT_2:92;
  dom (proj(A,i)) = (the carrier of S) by PARTFUN1:def 2;
  then
A12: rng (the_arity_of o) c= dom (proj(A,i));
  dom ((proj(A,i))#x) = dom ((Frege((proj(A,i))*the_arity_of o)).x) by
MSUALG_3:def 5
    .= dom (((proj(A,i))*the_arity_of o)..x) by A10,PRALG_2:def 2
    .= dom ((proj(A,i))*the_arity_of o) by PRALG_1:def 17
    .= dom (the_arity_of o) by A12,RELAT_1:27;
  hence thesis by A11,A5,FUNCT_1:2;
end;

theorem
  for i be Element of I for A be MSAlgebra-Family of I,S holds proj(A,i)
  is_homomorphism product A,A.i
proof
  let i be Element of I;
  let A be MSAlgebra-Family of I,S;
  thus proj(A,i) is_homomorphism product A,A.i
  proof
    let o be OperSymbol of S such that
    Args(o,product A) <> {};
    let x be Element of Args(o,product A);
    set F = proj(A,i), s = the_result_sort_of o;
    o in the carrier' of S;
    then
A1: o in dom (the ResultSort of S) by FUNCT_2:def 1;
A2: Result(o,product A) = ((the Sorts of product A) * the ResultSort of S)
    .o by MSUALG_1:def 5
      .= (the Sorts of product A).((the ResultSort of S).o) by A1,FUNCT_1:13
      .= (SORTS A).s by MSUALG_1:def 2
      .= product Carrier(A,s) by PRALG_2:def 10;
    thus (F.s).(Den(o,product A).x) = Den(o,A.i).(F#x)
    proof
      per cases;
      suppose
A3:     the_arity_of o = {};
        then const(o,product A) in product(Carrier(A,s)) by A2,Th5;
        then
A4:     const(o,product A) in dom (proj (Carrier(A,s),i)) by CARD_3:def 16;
A5:     Args(o,product A) = {{}} by A3,PRALG_2:4;
        then
A6:     x = {} by TARSKI:def 1;
        (F.s).(Den(o,product A).x) = (F.s).(const(o,product A)) by A5,
TARSKI:def 1
          .= (proj (Carrier(A,s),i)).(const(o,product A)) by Def2
          .= (const(o,product A)).i by A4,CARD_3:def 16
          .= const(o,A.i) by A3,Th9
          .= Den(o,A.i).(F#x) by A3,A6,Th11;
        hence thesis;
      end;
      suppose
A7:     the_arity_of o <> {};
        reconsider D = (Den(o,product A).x) as Function by A2;
        (Den(o,product A).x) in product Carrier(A,s) by A2;
        then
A8:     (Den(o,product A).x) in dom (proj (Carrier(A,s),i)) by CARD_3:def 16;
        (F.s).(Den(o,product A).x) = (proj (Carrier(A,s),i)).(Den(o,
        product A).x) by Def2
          .= D.i by A8,CARD_3:def 16
          .= (Den(o,A.i)).((commute x).i) by A7,Th22
          .= (Den(o,A.i)).(proj(A,i)#x) by A7,Th23;
        hence thesis;
      end;
    end;
  end;
end;

theorem Th25:
  for U1 be non-empty MSAlgebra over S for F being
  ManySortedFunction of I st (for i be Element of I holds ex F1 being
  ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds F
  in Funcs(I,Funcs(the carrier of S, {F.i9.s1 where s1 is SortSymbol of S,i9 is
  Element of I :not contradiction})) & (commute F).s.i = F.i.s
proof
  let U1 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
  st F1 = F.i & F1 is_homomorphism U1,A.i;
  set FS = {F.i9.s1 where s1 is SortSymbol of S,i9 is Element of I :not
  contradiction}, CA = the carrier of S;
A2: rng F c= Funcs(CA,FS)
  proof
    let x be set;
    assume x in rng F;
    then consider i9 be set such that
A3: i9 in dom F and
A4: F.i9 = x by FUNCT_1:def 3;
    reconsider i1 = i9 as Element of I by A3;
    consider F9 being ManySortedFunction of U1,A.i1 such that
A5: F9 = F.i1 and
    F9 is_homomorphism U1,A.i1 by A1;
A6: rng F9 c= FS
    proof
      let x9 be set;
      assume x9 in rng F9;
      then consider s9 be set such that
A7:   s9 in dom F9 and
A8:   F9.s9 = x9 by FUNCT_1:def 3;
      s9 is SortSymbol of S by A7;
      hence thesis by A5,A8;
    end;
    dom F9 = CA by PARTFUN1:def 2;
    hence thesis by A4,A5,A6,FUNCT_2:def 2;
  end;
A9: dom F = I by PARTFUN1:def 2;
  hence F in Funcs(I,Funcs(CA,FS)) by A2,FUNCT_2:def 2;
  F in Funcs(I,Funcs(CA,FS)) by A9,A2,FUNCT_2:def 2;
  hence thesis by FUNCT_6:56;
end;

theorem Th26:
  for U1 be non-empty MSAlgebra over S for F being
  ManySortedFunction of I st (for i be Element of I holds ex F1 being
  ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) holds (
commute F).s in Funcs(I,Funcs((the Sorts of U1).s, union {(the Sorts of A.i9).
  s1 where i9 is Element of I,s1 is SortSymbol of S : not contradiction}))
proof
  let U1 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
  st F1 = F.i & F1 is_homomorphism U1,A.i;
  set SU = the Sorts of U1, CA = the carrier of S, SA = union {(the Sorts of A
  .i9).s1 where i9 is Element of I,s1 is SortSymbol of S : not contradiction},
SA9 = {(the Sorts of A.i9).s1 where i9 is Element of I,s1 is SortSymbol of S :
not contradiction}, FS = {F.i9.s1 where s1 is SortSymbol of S,i9 is Element of
I: not contradiction};
  F in Funcs(I,Funcs(CA,FS)) by A1,Th25;
  then commute F in Funcs(CA,Funcs(I,FS)) by FUNCT_6:55;
  then consider F9 be Function such that
A2: F9 = commute F & dom F9 = CA and
A3: rng F9 c= Funcs(I,FS) by FUNCT_2:def 2;
  (commute F).s in rng F9 by A2,FUNCT_1:def 3;
  then
A4: ex F2 be Function st F2 = (commute F).s & dom F2 = I & rng F2 c= FS by A3,
FUNCT_2:def 2;
  rng ((commute F).s) c= Funcs(SU.s,SA)
  proof
    let x9 be set;
    assume x9 in rng ((commute F).s);
    then consider i9 be set such that
A5: i9 in dom ((commute F).s) and
A6: x9 = ((commute F).s).i9 by FUNCT_1:def 3;
    reconsider i1 = i9 as Element of I by A4,A5;
    consider F9 be ManySortedFunction of U1,A.i1 such that
A7: F9 = F.i1 and
    F9 is_homomorphism U1,A.i1 by A1;
    (the Sorts of A.i1).s c= SA
    proof
A8:   (the Sorts of A.i1).s in SA9;
      let y be set;
      assume y in (the Sorts of A.i1).s;
      hence thesis by A8,TARSKI:def 4;
    end;
    then
A9: dom (F9.s) = SU.s & rng (F9.s) c= SA by FUNCT_2:def 1,XBOOLE_1:1;
    x9 = F9.s by A1,A6,A7,Th25;
    hence thesis by A9,FUNCT_2:def 2;
  end;
  hence thesis by A4,FUNCT_2:def 2;
end;

theorem Th27:
  for U1 be non-empty MSAlgebra over S for F being
  ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for F9 be
ManySortedFunction of U1,A.i st F9 = F.i for x be set st x in (the Sorts of U1)
  .s for f be Function st f = (commute((commute F).s)).x holds f.i = F9.s.x
proof
  let U1 be non-empty MSAlgebra over S;
  set SU = the Sorts of U1, SA = union {(the Sorts of A.i9).s1 where i9 is
  Element of I,s1 is SortSymbol of S : not contradiction};
  let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
  st F1 = F.i & F1 is_homomorphism U1,A.i;
A2: (commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th26;
  then dom ((commute F).s) = I by FUNCT_2:92;
  then
A3: ((commute F).s).i in rng ((commute F).s) by FUNCT_1:def 3;
  reconsider f9 = (commute F).s as Function;
  rng ((commute F).s) c= Funcs(SU.s,SA) by A2,FUNCT_2:92;
  then consider g be Function such that
A4: g = f9.i and
  dom g = SU.s and
  rng g c= SA by A3,FUNCT_2:def 2;
  let F9 be ManySortedFunction of U1,A.i such that
A5: F9 = F.i;
  let x1 be set such that
A6: x1 in (the Sorts of U1).s;
  let f be Function such that
A7: f = (commute((commute F).s)).x1;
  g = F9.s by A1,A5,A4,Th25;
  hence thesis by A6,A7,A2,A4,FUNCT_6:56;
end;

theorem Th28:
  for U1 be non-empty MSAlgebra over S for F being
  ManySortedFunction of I st (for i be Element of I holds ex F1 being
ManySortedFunction of U1,A.i st F1 = F.i & F1 is_homomorphism U1,A.i) for x be
set st x in (the Sorts of U1).s holds (commute ((commute F).s)).x in product (
  Carrier(A,s))
proof
  let U1 be non-empty MSAlgebra over S;
  set SU = the Sorts of U1, SA = union {(the Sorts of A.i9).s1 where i9 is
  Element of I,s1 is SortSymbol of S : not contradiction};
  let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
  st F1 = F.i & F1 is_homomorphism U1,A.i;
  (commute F).s in Funcs (I,Funcs(SU.s,SA)) by A1,Th26;
  then commute ((commute F).s) in Funcs (SU.s,Funcs(I,SA)) by FUNCT_6:55;
  then consider f9 be Function such that
A2: f9 = (commute (commute F).s) and
A3: dom f9 = SU.s and
A4: rng f9 c= Funcs(I,SA) by FUNCT_2:def 2;
  let x be set such that
A5: x in (the Sorts of U1).s;
  f9.x in rng f9 by A5,A3,FUNCT_1:def 3;
  then consider f be Function such that
A6: f = (commute (commute F).s).x and
A7: dom f = I and
  rng f c= SA by A2,A4,FUNCT_2:def 2;
A8: now
    let i1 be set;
    assume i1 in dom ((Carrier(A,s)));
    then reconsider i9 = i1 as Element of I;
    consider F1 be ManySortedFunction of U1,A.i9 such that
A9: F1 = F.i9 and
    F1 is_homomorphism U1,A.i9 by A1;
    x in dom (F1.s) by A5,FUNCT_2:def 1;
    then
A10: (ex U0 being MSAlgebra over S st U0 = A.i9 & (Carrier(A,s )).i9 = (
    the Sorts of U0).s )& F1.s.x in rng (F1.s) by FUNCT_1:def 3,PRALG_2:def 9;
    f.i9 = F1.s.x by A1,A5,A6,A9,Th27;
    hence ((commute ((commute F).s)).x).i1 in ((Carrier(A,s))).i1 by A6,A10;
  end;
  dom ((commute (commute F).s).x) = dom (Carrier(A,s)) by A6,A7,PARTFUN1:def 2;
  hence thesis by A8,CARD_3:9;
end;

theorem
  for U1 be non-empty MSAlgebra over S for F being ManySortedFunction of
  I st (for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i st
F1 = F.i & F1 is_homomorphism U1,A.i) holds ex H being ManySortedFunction of U1
,(product A) st H is_homomorphism U1,(product A) & for i be Element of I holds
  proj(A,i) ** H = F.i
proof
  let U1 be non-empty MSAlgebra over S;
  let F be ManySortedFunction of I such that
A1: for i be Element of I holds ex F1 being ManySortedFunction of U1,A.i
  st F1 = F.i & F1 is_homomorphism U1,A.i;
  set SU = the Sorts of U1, CA = the carrier of S, SA = union {(the Sorts of A
  .i9).s1 where i9 is Element of I,s1 is SortSymbol of S : not contradiction};
  deffunc G(Element of S) = commute((commute F).$1);
  consider H being ManySortedSet of (the carrier of S) such that
A2: for s9 be Element of (the carrier of S) holds H.s9 = G(s9) from
  PBOOLE:sch 5;
  now
    let s9 be set;
    assume
A3: s9 in (the carrier of S);
    then reconsider s99 = s9 as SortSymbol of S;
    (commute F).s9 in Funcs (I,Funcs(SU.s9,SA)) by A1,A3,Th26;
    then commute ((commute F).s9) in Funcs (SU.s9,Funcs(I,SA)) by A3,FUNCT_6:55
;
    then H.s9 in Funcs(SU.s9,Funcs(I,SA)) by A2,A3;
    then consider Hs be Function such that
A4: Hs = H.s9 and
A5: dom Hs = SU.s9 and
A6: rng Hs c= Funcs(I,SA) by FUNCT_2:def 2;
    rng Hs c= (the Sorts of (product A)).s9
    proof
      let x be set;
      assume
A7:   x in rng Hs;
      then consider f be Function such that
A8:   f = x and
A9:   dom f = I and
      rng f c= SA by A6,FUNCT_2:def 2;
      consider x1 be set such that
A10:  x1 in dom Hs and
A11:  Hs.x1 = f by A7,A8,FUNCT_1:def 3;
A12:  now
        let i9 be set;
        assume i9 in dom Carrier(A,s99);
        then reconsider i99 = i9 as Element of I;
        consider F9 be ManySortedFunction of U1,A.i99 such that
A13:    F9 = F.i99 and
        F9 is_homomorphism U1,A.i99 by A1;
        H.s99 = commute ((commute F).s99) by A2;
        then
A14:    f.i99 = F9.s99.x1 by A1,A4,A5,A10,A11,A13,Th27;
        dom (F9.s99) = dom Hs by A5,FUNCT_2:def 1;
        then
A15:    F9.s9.x1 in rng (F9.s9) by A10,FUNCT_1:def 3;
        (ex U0 being MSAlgebra over S st U0 = A.i99 & (Carrier(A, s99)).
i99 =(the Sorts of U0).s99 )& rng (F9.s99) c= (the Sorts of A.i99).s99 by
PRALG_2:def 9;
        hence f.i9 in Carrier(A,s99).i9 by A14,A15;
      end;
      dom Carrier(A,s99) = dom f by A9,PARTFUN1:def 2;
      then f in product Carrier(A,s99) by A12,CARD_3:9;
      hence thesis by A8,PRALG_2:def 10;
    end;
    hence
    H.s9 is Function of (the Sorts of U1).s9, (the Sorts of (product A)).
    s9 by A3,A4,A5,FUNCT_2:def 1,RELSET_1:4;
  end;
  then reconsider H as ManySortedFunction of U1,(product A) by PBOOLE:def 15;
A16: H is_homomorphism U1,(product A)
  proof
    let o be OperSymbol of S such that
    Args(o,U1) <> {};
    let x be Element of Args(o,U1);
    set s9 = the_result_sort_of o;
A17: Result(o,U1) = (the Sorts of U1).(the_result_sort_of o) by PRALG_2:3;
    then
A18: (Den(o,U1).x) in SU.s9;
    thus (H.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,(product A)).(H#x)
    proof
      per cases;
      suppose
A19:    the_arity_of o = {};
        set f = (commute ((commute F).s9)).const(o,U1);
        Args(o,U1) = {{}} by A19,PRALG_2:4;
        then
A20:    x = {} by TARSKI:def 1;
A21:    now
          let i9 be set;
          assume i9 in I;
          then reconsider ii = i9 as Element of I;
          consider F1 be ManySortedFunction of U1,A.ii such that
A22:      F1 = F.ii and
A23:      F1 is_homomorphism U1,A.ii by A1;
A24:      F1#x = {} by A19,A20,Th11;
          thus f.i9 = (F1.(the_result_sort_of o)).(Den(o,U1).x) by A1,A17,A20
,A22,Th27
            .= const(o,A.ii) by A23,A24,MSUALG_3:def 7
            .= (const(o,product A)).i9 by A19,Th9;
        end;
        const(o,product A) in Funcs(I,union { Result(o,A.i1) where i1 is
        Element of I: not contradiction }) by A19,Th8;
        then
A25:    ex Co be Function st Co = const(o,product A) & dom Co = I & rng Co
c= union { Result(o,A.i1) where i1 is Element of I: not contradiction } by
FUNCT_2:def 2;
        f in product (Carrier(A,s9)) by A1,A18,A20,Th28;
        then dom f = dom (Carrier(A,s9)) by CARD_3:9
          .= I by PARTFUN1:def 2;
        then
A26:    f = const(o,product A) by A25,A21,FUNCT_1:2;
        H#x = {} by A19,A20,Th11;
        hence thesis by A2,A20,A26;
      end;
      suppose
A27:    the_arity_of o <> {};
A28:    Den(o,product A) = (OPS A).o by MSUALG_1:def 6
          .= IFEQ(the_arity_of o,{},commute(A?.o),Commute Frege(A?.o)) by
PRALG_2:def 13
          .= Commute Frege(A?.o) by A27,FUNCOP_1:def 8;
A29:    now
          let y be Element of Args(o,product A);
          (commute y) in product doms (A?.o) by A27,Th17;
          then
A30:      (commute y) in dom (Frege(A?.o)) by PARTFUN1:def 2;
          y in dom (Commute Frege(A?.o)) by A27,Th18;
          then Den(o,product A).y = (Frege(A?.o)).(commute y) by A28,
PRALG_2:def 1;
          hence Den(o,product A).y in rng (Frege(A?.o)) by A30,FUNCT_1:def 3;
        end;
        then reconsider f1 = Den(o,(product A)).(H#x) as Function by PRALG_2:8
;
        f1 in rng (Frege(A?.o)) by A29;
        then
A31:    dom f1 = I by PRALG_2:9;
        set D = union { (the Sorts of A.i9).ss where i9 is Element of I,ss is
        Element of (the carrier of S) : not contradiction };
        set f = (commute ((commute F).s9)).(Den(o,U1).x);
A32:    (H#x) in Funcs (dom (the_arity_of o),Funcs (I,D)) by Th14;
A33:    now
          let i9 be set;
          assume i9 in I;
          then reconsider ii = i9 as Element of I;
          consider F1 be ManySortedFunction of U1,A.ii such that
A34:      F1 = F.ii and
A35:      F1 is_homomorphism U1,A.ii by A1;
A36:      (F1.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,A.ii).(F1#x)
          by A35,MSUALG_3:def 7;
A37:      now
            let n be set;
            assume
A38:        n in dom (the_arity_of o);
            then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
            then reconsider
            s1 = (the_arity_of o).n as Element of (the carrier of S
            );
A39:        (F1#x).n = F1.((the_arity_of o)/.n).(x.n) by A38,Th13
              .= F1.s1.(x.n) by A38,PARTFUN1:def 6;
            x in Args(o,U1);
            then
A40:        x in product ((the Sorts of U1)*(the_arity_of o)) by PRALG_2:3;
            then
A41:        dom x = dom ((the Sorts of U1)*(the_arity_of o)) by CARD_3:9;
A42:        dom x = dom ((the Sorts of U1)*(the_arity_of o)) by A40,CARD_3:9
              .= dom (the_arity_of o) by PRALG_2:3;
            then x.n in ((the Sorts of U1)*(the_arity_of o)).n by A38,A40,A41,
CARD_3:9;
            then
A43:        (x.n) in SU.s1 by A38,A42,A41,FUNCT_1:12;
A44:        (H#x).n = H.((the_arity_of o)/.n).(x.n) by A38,Th13
              .= H.s1.(x.n) by A38,PARTFUN1:def 6
              .= (commute ((commute F).s1)).(x.n) by A2;
            then reconsider g = (H#x).n as Function;
            thus ((commute (H#x)).ii).n = g.ii by A32,A38,FUNCT_6:56
              .= (F1#x).n by A1,A34,A43,A39,A44,Th27;
          end;
          dom F1 = (the carrier of S) by PARTFUN1:def 2;
          then
A45:      rng (the_arity_of o) c= dom F1;
          commute (H#x) in Funcs (I,Funcs (dom(the_arity_of o),D)) by A27,A32,
FUNCT_6:55;
          then consider ff be Function such that
A46:      ff = commute (H#x) and
A47:      dom ff = I and
A48:      rng ff c= Funcs (dom(the_arity_of o),D) by FUNCT_2:def 2;
          ff.ii in rng ff by A47,FUNCT_1:def 3;
          then
A49:      ex gg be Function st gg = (commute (H#x)).ii & dom gg = dom(
          the_arity_of o) & rng gg c= D by A46,A48,FUNCT_2:def 2;
A50:      x in product doms (F1*the_arity_of o) by Th12;
          dom (F1#x) = dom ((Frege(F1*the_arity_of o)).x) by MSUALG_3:def 5
            .= dom ((F1*the_arity_of o)..x) by A50,PRALG_2:def 2
            .= dom (F1*the_arity_of o) by PRALG_1:def 17
            .= dom (the_arity_of o) by A45,RELAT_1:27;
          then F1#x = (commute (H#x)).ii by A49,A37,FUNCT_1:2;
          then f.i9 = Den(o,A.ii).((commute (H#x)).ii) by A1,A17,A34,A36,Th27
            .= f1.i9 by A27,Th22;
          hence f.i9 = f1.i9;
        end;
        (commute ((commute F).s9)).(Den(o,U1).x) in product(Carrier(A,s9)
        ) by A1,A17,Th28;
        then dom f = dom (Carrier(A,s9)) by CARD_3:9
          .= I by PARTFUN1:def 2;
        then (commute ((commute F).s9)).(Den(o,U1).x) = f1 by A31,A33,FUNCT_1:2
;
        hence thesis by A2;
      end;
    end;
  end;
  take H;
  for i be Element of I holds proj(A,i) ** H = F.i
  proof
    let i be Element of I;
    consider F1 be ManySortedFunction of U1,A.i such that
A51: F1 = F.i and
    F1 is_homomorphism U1,A.i by A1;
A52: dom(proj(A,i) ** H) = (dom proj(A,i)) /\ (dom H) by PBOOLE:def 19
      .= CA /\ (dom H) by PARTFUN1:def 2
      .= CA /\ CA by PARTFUN1:def 2
      .= CA;
A53: now
      let s9 be set;
      assume s9 in CA;
      then reconsider s1 = s9 as SortSymbol of S;
A54:  (proj(A,i) ** H).s9 = (proj(A,i).s1)*(H.s1) by A52,PBOOLE:def 19
        .= (proj (Carrier(A,s1),i)) * (H.s1) by Def2
        .= ((proj (Carrier(A,s1),i))) * (commute (commute F).s1) by A2;
      (commute F).s1 in Funcs (I,Funcs(SU.s1,SA)) by A1,Th26;
      then commute ((commute F).s1) in Funcs (SU.s1,Funcs(I,SA)) by FUNCT_6:55;
      then consider f9 be Function such that
A55:  f9 = (commute (commute F).s1) and
A56:  dom f9 = SU.s1 and
      rng f9 c= Funcs(I,SA) by FUNCT_2:def 2;
      rng f9 c= dom (proj (Carrier(A,s1),i))
      proof
        let y be set;
        assume y in rng f9;
        then consider x9 be set such that
A57:    x9 in dom f9 and
A58:    f9.x9 = y by FUNCT_1:def 3;
        (commute (commute F).s1).x9 in product (Carrier(A,s1)) by A1,A56,A57
,Th28;
        hence thesis by A55,A58,CARD_3:def 16;
      end;
      then
A59:  dom ((proj(A,i) ** H).s9) = SU.s9 by A55,A56,A54,RELAT_1:27;
A60:  now
        let x be set;
        assume
A61:    x in SU.s9;
        then ((commute (commute F).s1).x) in product (Carrier(A,s1)) by A1,Th28
;
        then
A62:    ((commute (commute F).s1).x) in dom (proj (Carrier(A,s1),i )) by
CARD_3:def 16;
        thus ((proj(A,i) ** H).s9).x = (proj (Carrier(A,s1),i)).((commute (
        commute F).s1).x) by A54,A59,A61,FUNCT_1:12
          .= ((commute (commute F).s1).x).i by A62,CARD_3:def 16
          .= F1.s9.x by A1,A51,A61,Th27;
      end;
      dom (F1.s9) = dom (F1.s1) .= SU.s9 by FUNCT_2:def 1;
      hence (proj(A,i) ** H).s9 = F1.s9 by A59,A60,FUNCT_1:2;
    end;
    dom F1 = CA by PARTFUN1:def 2;
    hence thesis by A51,A52,A53,FUNCT_1:2;
  end;
  hence thesis by A16;
end;

begin :: The Class of Family of Many Sorted Algebras

definition
  let I,J,S;
  mode MSAlgebra-Class of S,J -> ManySortedSet of I means
    :Def3:
    for i be set st i in I holds it.i is MSAlgebra-Family of J.i,S;
  existence
  proof
    defpred P[set,set] means $2 is MSAlgebra-Family of J.$1,S;
A1: for i be set st i in I ex F be set st P[i,F]
    proof
      let i be set such that
      i in I;
      set F = the MSAlgebra-Family of J.i,S;
      take F;
      thus thesis;
    end;
    consider C be ManySortedSet of I such that
A2: for i be set st i in I holds P[i,C.i] from PBOOLE:sch 3(A1);
    take C;
    thus thesis by A2;
  end;
end;

definition
  let I,S,A,EqR;
  func A / EqR -> MSAlgebra-Class of S,id (Class EqR) means
  :Def4:
  for c st c in Class EqR holds it.c = A|c;
  existence
  proof
    thus ex X be MSAlgebra-Class of S,id Class EqR st for c st c in Class EqR
    holds X.c = A|c
    proof
      deffunc F(set) = A|$1;
      consider X be ManySortedSet of Class EqR such that
A1:   for c st c in Class EqR holds X.c = F(c) from PBOOLE:sch 4;
      X is MSAlgebra-Class of S,id Class EqR
      proof
        let c be set;
        assume
A2:     c in Class EqR;
A3:     dom (A|c) = (dom A) /\ c by RELAT_1:61
          .= I /\ c by PARTFUN1:def 2
          .= c by A2,XBOOLE_1:28
          .= (id Class EqR).c by A2,FUNCT_1:18;
        then reconsider ac = A|c as ManySortedSet of (id Class EqR).c by
PARTFUN1:def 2,RELAT_1:def 18;
        ac is MSAlgebra-Family of (id Class EqR).c,S
        proof
          let i be set;
          assume
A4:       i in (id Class EqR).c;
          dom ac = c by A2,A3,FUNCT_1:18;
          then reconsider i9 = i as Element of I by A2,A3,A4;
          A.i9 is non-empty MSAlgebra over S;
          hence thesis by A3,A4,FUNCT_1:47;
        end;
        hence thesis by A1,A2;
      end;
      then reconsider X as MSAlgebra-Class of S,id Class EqR;
      take X;
      thus thesis by A1;
    end;
  end;
  uniqueness
  proof
    for X, Y be MSAlgebra-Class of S,id Class EqR st (for c st c in Class
    EqR holds X.c = A|c) & for c st c in Class EqR holds Y.c = A|c holds X = Y
    proof
      let X, Y be MSAlgebra-Class of S,id Class EqR such that
A5:   for c st c in Class EqR holds X.c = A|c and
A6:   for c st c in Class EqR holds Y.c = A|c;
      now
        let c;
        assume
A7:     c in Class EqR;
        hence X.c = A|c by A5
          .= Y.c by A6,A7;
      end;
      hence thesis by PBOOLE:3;
    end;
    hence thesis;
  end;
end;

definition
  let I,S;
  let J be non-empty ManySortedSet of I;
  let C be MSAlgebra-Class of S,J;
  func product C -> MSAlgebra-Family of I,S means
  :Def5:
  for i st i in I ex Ji
be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & it.i
  = product Cs;
  existence
  proof
    thus ex PC be MSAlgebra-Family of I,S st for i st i in I ex Ji be non
    empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC.i =
    product Cs
    proof
      defpred P[set,set] means ex Ji be non empty set, Cs be MSAlgebra-Family
      of Ji,S st Ji = J.$1 & Cs = C.$1 & $2 = product Cs;
A1:   now
        let i be set;
        assume
A2:     i in I;
        then reconsider Ji = J.i as non empty set;
        reconsider Cs = C.i as MSAlgebra-Family of Ji,S by A2,Def3;
        ex a be set st a = product Cs;
        then consider j be set such that
A3:     ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji =
        J.i & Cs = C.i & j = product Cs;
        take j;
        thus P[i,j] by A3;
      end;
      consider PC be ManySortedSet of I such that
A4:   for i be set st i in I holds P[i,PC.i] from PBOOLE:sch 3(A1);
      now
        let i be set;
        assume i in I;
        then
        ex Ji be non empty set, Cs be MSAlgebra-Family of Ji,S st Ji = J.i
        & Cs = C.i & PC.i = product Cs by A4;
        hence PC.i is non-empty MSAlgebra over S;
      end;
      then reconsider PC as MSAlgebra-Family of I,S by PRALG_2:def 5;
      take PC;
      thus thesis by A4;
    end;
  end;
  uniqueness
  proof
    for PC1,PC2 be MSAlgebra-Family of I,S st (for i st i in I ex Ji be
non empty set , Cs be MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i =
product Cs ) & for i st i in I ex Ji be non empty set , Cs be MSAlgebra-Family
    of Ji,S st Ji =J.i & Cs = C.i & PC2.i = product Cs holds PC1 = PC2
    proof
      let PC1,PC2 be MSAlgebra-Family of I,S such that
A5:   ( for i st i in I ex Ji be non empty set , Cs be
MSAlgebra-Family of Ji,S st Ji = J.i & Cs = C.i & PC1.i = product Cs)& for i st
i in I ex Ji be non empty set , Cs be MSAlgebra-Family of Ji,S st Ji =J.i & Cs
      = C.i & PC2.i = product Cs;
      now
        let i1 be set;
        assume i1 in I;
        then reconsider i9 = i1 as Element of I;
        (ex Ji1 be non empty set, Cs1 be MSAlgebra-Family of Ji1,S st Ji1
= J.i9 & Cs1 = C.i9 & PC1.i9 = product Cs1 )& ex Ji2 be non empty set, Cs2 be
MSAlgebra-Family of Ji2,S st Ji2 = J.i9 & Cs2 = C.i9 & PC2.i9 = product Cs2 by
A5;
        hence PC1.i1 = PC2.i1;
      end;
      hence thesis by PBOOLE:3;
    end;
    hence thesis;
  end;
end;

theorem
  for A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I
  holds product A, product (product (A/EqR)) are_isomorphic
proof
  let A be MSAlgebra-Family of I,S, EqR be Equivalence_Relation of I;
  set U1 = product A, U2 = product product (A/EqR);
  set U19 = the Sorts of U1, U29 = the Sorts of U2;
  defpred P[set,set,set] means for f1,g1 being Function st f1 = $2 & g1 = $1
  for e being Element of Class EqR holds g1.e = f1|e;
A1: for s be set st s in the carrier of S holds for x be set st x in U19.s
  ex y be set st y in U29.s & P[y,x,s]
  proof
    let s be set;
    assume s in the carrier of S;
    then reconsider s9 = s as SortSymbol of S;
A2: U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
    let x be set such that
A3: x in U19.s;
    reconsider x as Function by A3,A2;
    deffunc F(set) = x|$1;
    consider y being ManySortedSet of Class EqR such that
A4: for c st c in Class EqR holds y.c = F(c) from PBOOLE:sch 4;
A5: dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2;
A6: for a be set st a in dom (Carrier(product (A/EqR),s9)) holds y.a in (
    Carrier(product (A/EqR),s9)).a
    proof
      set A9 = product (A/EqR);
      let a be set such that
A7:   a in dom (Carrier(product (A/EqR),s9));
A8:   (A/EqR).a = A|a by A7,Def4;
      reconsider a as non empty Subset of I by A5,A7;
A9:   ex U0 being MSAlgebra over S st U0 = A9.a & (Carrier(A9, s9)).a = (
      the Sorts of U0).s9 by A7,PRALG_2:def 9;
A10:  dom (A|a) = dom A /\ a by RELAT_1:61
        .= I /\ a by PARTFUN1:def 2
        .= a by XBOOLE_1:28;
      then reconsider Aa1 = A|a as ManySortedSet of a by PARTFUN1:def 2;
      for i be set st i in a holds Aa1.i is non-empty MSAlgebra over S
      proof
        let i be set;
        assume
A11:    i in a;
        then A.i is non-empty MSAlgebra over S by PRALG_2:def 5;
        hence thesis by A10,A11,FUNCT_1:47;
      end;
      then reconsider Aa = Aa1 as MSAlgebra-Family of a,S by PRALG_2:def 5;
      x|a in product((Carrier(A,s9))|a) by A3,A2,Th1;
      then
A12:  x|a in product (Carrier(Aa,s9)) by Th2;
      consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such that
A13:  Ji = (id Class EqR).a and
A14:  Cs = (A/EqR).a & A9.a = product Cs by A7,Def5;
      Ji = a by A7,A13,FUNCT_1:18;
      then (Carrier(A9,s9)).a = product (Carrier(Aa,s9)) by A8,A14,A9,
PRALG_2:def 10;
      hence thesis by A4,A7,A12;
    end;
    take y;
    dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2
      .= dom y by PARTFUN1:def 2;
    then y in product Carrier(product (A/EqR),s9) by A6,CARD_3:9;
    hence thesis by A4,PRALG_2:def 10;
  end;
  consider F be ManySortedFunction of U19, U29 such that
A15: for s be set st s in the carrier of S holds ex f be Function of U19
  .s, U29.s st f = F.s & for x be set st x in U19.s holds P[f.x,x,s] from
  MSSUBFAM:sch 1(A1);
A16: F is_homomorphism U1,U2
  proof
    let o be OperSymbol of S such that
    Args(o,U1) <> {};
    let x be Element of Args(o,U1);
    thus (F.(the_result_sort_of o)).(Den(o,U1).x) = Den(o,U2).(F#x)
    proof
A17:  Den(o,U1).x in Result(o,U1);
      then
A18:  Den(o,U1).x in U19.(the_result_sort_of o) by PRALG_2:3;
      set s = the_result_sort_of o, U3 = product (A/EqR);
A19:  U29.s = product Carrier(U3,s) by PRALG_2:def 10;
A20:  ex f be Function of U19.s, U29.s st f = F.s & for x9 be set st x9 in
      U19.s holds P[f.x9,x9,s] by A15;
A21:  dom (F.s) = (SORTS A).s by FUNCT_2:def 1
        .= product Carrier(A,s) by PRALG_2:def 10;
A22:  Den(o,U1).x in product Carrier(A,s) by Th19;
      per cases;
      suppose
A23:    the_arity_of o = {};
        then Args(o,U1) = {{}} by PRALG_2:4;
        then
A24:    x = {} by TARSKI:def 1;
        then
A25:    F.s.const(o,U1) in rng (F.s) by A21,A22,FUNCT_1:def 3;
        reconsider g1 = F.s.const(o,U1) as Function by A19;
A26:    dom (const(o,U1)) = dom Carrier(A,s) by A22,A24,CARD_3:9
          .= I by PARTFUN1:def 2;
A27:    now
          let e be Element of Class EqR;
          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
          that
A28:      Ji = (id Class EqR).e and
A29:      Cs = (A/EqR).e and
A30:      U3.e = product Cs by Def5;
A31:      dom (const(o,product A)|e) = I /\ e by A26,RELAT_1:61
            .= e by XBOOLE_1:28;
A32:      now
            let i1 be set;
A33:        dom(A|e) = dom A /\ e by RELAT_1:61
              .= I /\ e by PARTFUN1:def 2
              .= e by XBOOLE_1:28;
            assume
A34:        i1 in e;
            then reconsider ii = i1 as Element of Ji by A28,FUNCT_1:18;
            reconsider ii9 = ii as Element of I by A34;
            Cs = A|e by A29,Def4;
            then
A35:        Cs.ii = A.ii9 by A34,A33,FUNCT_1:47;
            thus (const(o,product A)|e).i1 = const(o,product A).i1 by A31,A34,
FUNCT_1:47
              .= const(o,A.ii9) by A23,Th9
              .= const(o,product Cs).i1 by A23,A35,Th9;
          end;
          const(o,product Cs) in Funcs(Ji, union { Result(o,Cs.i9) where
          i9 is Element of Ji: not contradiction }) by A23,Th8;
          then dom (const(o,product Cs)) = Ji by FUNCT_2:92
            .= e by A28,FUNCT_1:18;
          hence const(o,U1)|e = const(o,U3.e) by A30,A31,A32,FUNCT_1:2;
        end;
A36:    const(o,U1) in U19.(the_result_sort_of o) by A17,A24,PRALG_2:3;
A37:    now
          let x1 be set;
          consider f1 be Function such that
A38:      f1 = const(o,U1);
          assume x1 in Class EqR;
          then reconsider e = x1 as Element of Class EqR;
          g1.e = f1|e by A20,A36,A38;
          hence g1.x1 = const(o,U3.e) by A27,A38
            .= const(o,product U3).x1 by A23,Th9;
        end;
        const(o,U2) in Funcs(Class EqR, union { Result(o,U3.i9) where i9
        is Element of Class EqR: not contradiction }) by A23,Th8;
        then
A39:    dom const(o,U2) = Class EqR by FUNCT_2:92;
        dom g1 = dom (Carrier(U3,s)) by A19,A25,CARD_3:9
          .= Class EqR by PARTFUN1:def 2;
        then F.s.const(o,U1) = const(o,U2) by A39,A37,FUNCT_1:2;
        hence thesis by A23,A24,Th11;
      end;
      suppose
A40:    the_arity_of o <> {};
A41:    Den(o,U2).(F#x) in product Carrier(U3,s) by Th19;
        then reconsider f1 = Den(o,U2).(F#x) as Function;
A42:    dom f1 = dom (Carrier(U3,s)) by A41,CARD_3:9
          .= Class EqR by PARTFUN1:def 2;
A43:    (F.s).(Den(o,U1).x) in rng (F.s) by A21,A22,FUNCT_1:def 3;
        reconsider g1 = (F.s).(Den(o,U1).x) as Function by A19;
A44:    now
          let e be Element of Class EqR;
          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
          that
A45:      Ji = (id Class EqR).e and
A46:      Cs = (A/EqR).e and
A47:      U3.e = product Cs by Def5;
A48:      (commute (F#x)).e is Element of Args(o,U3.e) by A40,Th20;
          then
A49:      Den (o,U3.e).((commute (F#x)).e) in product Carrier(Cs,s) by A47,Th19
;
          then reconsider f3 = Den(o,U3.e).((commute (F#x)).e) as Function;
A50:      now
            let i1 be Element of I;
            assume
A51:        i1 in e;
            then reconsider i2 = i1 as Element of Ji by A45,FUNCT_1:18;
A52:        now
              let n be set;
              assume
A53:          n in dom (the_arity_of o);
              then (the_arity_of o).n in rng (the_arity_of o) by FUNCT_1:def 3;
              then reconsider s1 = (the_arity_of o).n as SortSymbol of S;
A54:          x.n in product Carrier(A,(the_arity_of o)/.n) by A53,Th15;
              then reconsider f4 = x.n as Function;
A55:          x.n in product Carrier(A,s1) by A53,A54,PARTFUN1:def 6;
              then
A56:          x.n in (SORTS A).s1 by PRALG_2:def 10;
              dom f4 = dom (Carrier(A,s1)) by A55,CARD_3:9
                .= I by PARTFUN1:def 2;
              then
A57:          dom (f4|e) = I /\ e by RELAT_1:61
                .= e by XBOOLE_1:28;
              (F#x).n in product Carrier (U3,(the_arity_of o)/.n) by A53,Th15;
              then reconsider f5 = (F#x).n as Function;
              consider f7 be Function of U19.s1, U29.s1 such that
A58:          f7 = F.s1 and
A59:          for x9 be set st x9 in U19.s1 holds P[f7.x9,x9,s1] by A15;
              f5 = F.((the_arity_of o)/.n).(x.n) by A53,Th13
                .= f7.(x.n) by A53,A58,PARTFUN1:def 6;
              then
A60:          f5.e = f4|e by A56,A59;
              then reconsider f6 = f5.e as Function;
              f6 = ((commute (F#x)).e).n by A53,Th21;
              hence
              ((commute((commute (F#x)).e)).i1).n = (f4|e).i2 by A47,A48,A53
,A60,Th21
                .= f4.i2 by A51,A57,FUNCT_1:47
                .= ((commute x).i1).n by A53,Th21;
            end;
            (commute x).i1 is Element of Args(o,A.i1) by A40,Th20;
            then (commute x).i1 in Args(o,A.i1);
            then (commute x).i1 in product ((the Sorts of A.i1)*(the_arity_of
            o)) by PRALG_2:3;
            then
A61:        dom ((commute x).i1) = dom ((the Sorts of A.i1)*(the_arity_of
            o)) by CARD_3:9
              .= dom (the_arity_of o) by PRALG_2:3;
            (commute ((commute (F#x)).e)).i2 is Element of Args(o,Cs.i2)
            by A40,A47,A48,Th20;
            then (commute ((commute (F#x)).e)).i2 in Args(o,Cs.i2);
            then
            (commute ((commute (F#x)).e)).i2 in product ((the Sorts of Cs
            .i2)*(the_arity_of o)) by PRALG_2:3;
            then dom ((commute ((commute (F#x)).e)).i1) = dom ((the Sorts of
            Cs.i2)*(the_arity_of o)) by CARD_3:9
              .= dom (the_arity_of o) by PRALG_2:3;
            hence ((commute ((commute (F#x)).e)).i1) = ((commute x).i1) by A61
,A52,FUNCT_1:2;
          end;
          let f2 be Function such that
A62:      f2 = Den(o,U1).x;
          dom f2 = dom (Carrier(A,s)) by A22,A62,CARD_3:9
            .= I by PARTFUN1:def 2;
          then
A63:      dom (f2|e) = I /\ e by RELAT_1:61
            .= e by XBOOLE_1:28;
A64:      (commute (F#x)).e is Element of Args(o,product Cs) by A40,A47,Th20;
A65:      now
            let x1 be set;
A66:        dom(A|e) = dom A /\ e by RELAT_1:61
              .= I /\ e by PARTFUN1:def 2
              .= e by XBOOLE_1:28;
            assume
A67:        x1 in e;
            then reconsider i2 = x1 as Element of Ji by A45,FUNCT_1:18;
            reconsider i1 = i2 as Element of I by A67;
            Cs = A|e by A46,Def4;
            then Cs.i2 = A.i1 by A67,A66,FUNCT_1:47;
            hence
            f3.x1 = Den(o,A.i1).((commute ((commute (F#x)).e)).i2) by A40,A47
,A64,Th22
              .= Den(o,A.i1).((commute x).i1) by A50,A67
              .= f2.x1 by A40,A62,Th22
              .= (f2|e).x1 by A63,A67,FUNCT_1:47;
          end;
          dom f3 = dom (Carrier(Cs,s)) by A49,CARD_3:9
            .= Ji by PARTFUN1:def 2
            .= e by A45,FUNCT_1:18;
          hence f2|e = Den(o,U3.e).((commute (F#x)).e) by A63,A65,FUNCT_1:2;
        end;
A68:    now
          reconsider f2 = Den(o,U1).x as Function by A22;
          let x1 be set;
          assume x1 in Class EqR;
          then reconsider e = x1 as Element of Class EqR;
          g1.e = f2|e by A20,A18;
          hence g1.x1 = Den(o,U3.e).((commute (F#x)).e) by A44
            .= f1.x1 by A40,Th22;
        end;
        dom g1 = dom (Carrier(U3,s)) by A19,A43,CARD_3:9
          .= Class EqR by PARTFUN1:def 2;
        hence thesis by A42,A68,FUNCT_1:2;
      end;
    end;
  end;
  F is "1-1"
  proof
    let s be set, g be Function such that
A69: s in dom F and
A70: F.s = g;
    consider f being Function of U19.s, U29.s such that
A71: f = F.s and
A72: for x be set st x in U19.s holds P[f.x,x,s] by A15,A69;
    let x1,x2 be set such that
A73: x1 in dom g and
A74: x2 in dom g and
A75: g.x1 = g.x2;
A76: dom f = dom g by A70,A71;
    thus x1 = x2
    proof
      reconsider s9 = s as SortSymbol of S by A69;
A77:  U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
      then
A78:  ex gg be Function st x1 = gg & dom gg = dom Carrier(A,s9 ) & for x9
be set st x9 in dom Carrier(A,s9) holds gg.x9 in (Carrier(A,s9)).x9 by A73,A76,
CARD_3:def 5;
A79:  ex gg1 be Function st x2 = gg1 & dom gg1 = dom Carrier(A,s9) & for
x9 be set st x9 in dom Carrier(A,s9) holds gg1.x9 in (Carrier(A,s9) ).x9 by A74
,A76,A77,CARD_3:def 5;
      reconsider x2 as Function by A74,A76,A77;
A80:  dom x2 = I by A79,PARTFUN1:def 2;
      reconsider x1 as Function by A73,A76,A77;
A81:  U29.s = product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
A82:  for i be set st i in I holds x1.i = x2.i
      proof
        reconsider f99 = f.x2 as Function by A81;
        let i be set;
        assume
A83:    i in I;
        then
A84:    Class(EqR,i) is Element of Class EqR by EQREL_1:def 3;
        then x1|(Class(EqR,i)) = f99.(Class(EqR,i)) by A70,A73,A75,A71,A72,A76
          .= x2|(Class(EqR,i)) by A74,A72,A76,A84;
        then x1.i = (x2|(Class(EqR,i))).i by A83,EQREL_1:20,FUNCT_1:49
          .= x2.i by A83,EQREL_1:20,FUNCT_1:49;
        hence thesis;
      end;
      dom x1 = I by A78,PARTFUN1:def 2;
      hence thesis by A80,A82,FUNCT_1:2;
    end;
  end;
  then
A85: F is_monomorphism U1,U2 by A16,MSUALG_3:def 9;
  F is "onto"
  proof
    let s be set such that
A86: s in the carrier of S;
    reconsider s9 = s as SortSymbol of S by A86;
    consider f be Function of U19.s, U29.s such that
A87: f = F.s and
A88: for x be set st x in U19.s holds P[f.x,x,s] by A15,A86;
A89: U19.s9 = product Carrier(A,s9) by PRALG_2:def 10;
    for y be set holds y in (U29.s) iff ex x be set st x in dom f & y = f.x
    proof
      let y be set;
A90:  y in (U29.s) implies ex x be set st x in dom f & y = f.x
      proof
        assume y in (U29.s);
        then
A91:    y in product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
        then
A92:    ex gg be Function st y = gg & dom gg = dom (Carrier( product (A/
EqR),s9)) & for x9 be set st x9 in dom (Carrier(product (A/EqR),s9) ) holds gg.
        x9 in (Carrier(product (A/EqR),s9)).x9 by CARD_3:def 5;
        reconsider y as Function by A91;
        defpred Q[set,set] means ex e being Element of Class EqR, f being
        Function st $1 in e & f = y.e & $2 = f.$1;
A93:    for i be set st i in I ex j being set st Q[i,j]
        proof
          let i be set such that
A94:      i in I;
          Class(EqR,i) in Class EqR by A94,EQREL_1:def 3;
          then consider e be Element of Class EqR such that
A95:      e = Class(EqR,i);
          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
          that
          Ji = (id Class EqR).e and
          Cs = (A/EqR).e and
A96:      (product (A/EqR)).e = product Cs by Def5;
          ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
          then dom (Carrier(product (A/EqR),s9)) = Class EqR & (Carrier(
product (A/EqR),s9) ).e = product Carrier(Cs,s9) by A96,PARTFUN1:def 2
,PRALG_2:def 10;
          then reconsider y9 = y.e as Function by A92,Lm1;
          Q[i,y9.i] by A94,A95,EQREL_1:20;
          hence thesis;
        end;
        consider x being ManySortedSet of I such that
A97:    for i be set st i in I holds Q[i,x.i] from PBOOLE:sch 3(A93
        );
A98:    dom Carrier(product (A/EqR),s9) = Class EqR by PARTFUN1:def 2;
A99:    for z be set st z in dom Carrier(A,s9) holds x.z in (Carrier(A, s9)).z
        proof
          let z be set;
          assume z in dom Carrier(A,s9);
          then z in I;
          then consider
          e being Element of Class EqR,f1 being Function such that
A100:     z in e and
A101:     f1 = y.e & x.z = f1.z by A97;
          dom ((Carrier(A,s9))|e) = dom Carrier(A,s9) /\ e by RELAT_1:61
            .= I /\ e by PARTFUN1:def 2
            .= e by XBOOLE_1:28;
          then
A102:     ((Carrier(A,s9))|e).z = (Carrier(A,s9)).z by A100,FUNCT_1:47;
          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
          that
A103:     Ji = (id Class EqR).e and
A104:     Cs = (A/EqR).e and
A105:     (product (A/EqR)).e = product Cs by Def5;
          Cs = A|e & Ji = e by A103,A104,Def4,FUNCT_1:18;
          then
A106:     Carrier(Cs,s9) = (Carrier(A,s9))|e by Th2;
          ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
          then
A107:     (Carrier(product (A/EqR),s9)).e = product Carrier(Cs,s9) by A105,
PRALG_2:def 10;
          y.e in (Carrier(product (A/EqR),s9)).e by A92,A98;
          then
A108:     ex g be Function st y.e = g & dom g = dom Carrier(Cs,s9) & for
x9 be set st x9 in dom Carrier(Cs,s9) holds g.x9 in (Carrier(Cs,s9)).x9 by A107
,CARD_3:def 5;
          dom Carrier(Cs,s9) = Ji by PARTFUN1:def 2
            .= e by A103,FUNCT_1:18;
          hence thesis by A100,A101,A108,A102,A106;
        end;
        dom x = I by PARTFUN1:def 2
          .= dom Carrier(A,s9) by PARTFUN1:def 2;
        then
A109:   x in U19.s9 by A89,A99,CARD_3:9;
        then
A110:   x in dom f by FUNCT_2:def 1;
        then f.x in rng f by FUNCT_1:def 3;
        then f.x in U29.s;
        then
A111:   f.x in product Carrier(product (A/EqR),s9) by PRALG_2:def 10;
        then reconsider f9 = f.x as Function;
A112:   for e be set st e in Class EqR holds y.e = f9.e
        proof
          let e be set;
          assume e in Class EqR;
          then reconsider e as Element of Class EqR;
          consider Ji be non empty set, Cs be MSAlgebra-Family of Ji,S such
          that
A113:     Ji = (id Class EqR).e and
          Cs = (A/EqR).e and
A114:     (product (A/EqR)).e = product Cs by Def5;
          ex U0 being MSAlgebra over S st U0 = (product (A/EqR)).e & (
Carrier(product (A/EqR),s9)).e = (the Sorts of U0).s9 by PRALG_2:def 9;
          then
A115:     (Carrier(product (A/EqR),s9)).e = product Carrier(Cs,s9) by A114,
PRALG_2:def 10;
A116:     y.e in (Carrier(product (A/EqR),s9)).e by A92,A98;
          then reconsider y9 = y.e as Function by A115;
A117:     dom (x|e) = dom x /\ e by RELAT_1:61
            .= I /\ e by PARTFUN1:def 2
            .= e by XBOOLE_1:28;
A118:     for i be set st i in e holds (x|e).i = y9.i
          proof
            let i be set;
            assume
A119:       i in e;
            then consider
            e1 being Element of Class EqR,f1 being Function such that
A120:       i in e1 and
A121:       f1 = y.e1 & x.i = f1.i by A97;
            e = e1 by A119,A120,Th3;
            hence thesis by A117,A119,A121,FUNCT_1:47;
          end;
          ex g be Function st y.e = g & dom g = dom Carrier(Cs,s9) & for
x9 be set st x9 in dom Carrier(Cs,s9) holds g.x9 in (Carrier(Cs,s9)).x9 by A116
,A115,CARD_3:def 5;
          then dom y9 = Ji by PARTFUN1:def 2
            .= e by A113,FUNCT_1:18;
          then x|e = y9 by A117,A118,FUNCT_1:def 11;
          hence thesis by A88,A109;
        end;
        ex gg9 be Function st f.x = gg9 & dom gg9 = dom (Carrier (product
(A/EqR),s9)) & for x9 be set st x9 in dom (Carrier(product (A/EqR),s9 )) holds
        gg9.x9 in (Carrier(product (A/EqR),s9)).x9 by A111,CARD_3:def 5;
        then y = f9 by A92,A98,A112,FUNCT_1:def 11;
        hence thesis by A110;
      end;
      (ex x be set st x in dom f & y = f.x) implies y in (U29.s)
      proof
        given x be set such that
A122:   x in dom f and
A123:   y = f.x;
        f.x in rng f by A122,FUNCT_1:def 3;
        hence thesis by A123;
      end;
      hence y in (U29.s) iff ex x be set st x in dom f & y = f.x by A90;
    end;
    hence thesis by A87,FUNCT_1:def 3;
  end;
  then F is_epimorphism U1,U2 by A16,MSUALG_3:def 8;
  then F is_isomorphism U1,U2 by A85,MSUALG_3:def 10;
  hence thesis by MSUALG_3:def 11;
end;