:: Institution of Many-sorted Algebras, Part { I } : Signature Reduct
:: of an Algebra
::  by Grzegorz Bancerek
::
:: Received December 30, 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, STRUCT_0, MSUALG_1, RELAT_1, PBOOLE, MSATERM, MSAFREE,
      SUBSET_1, DTCONSTR, FINSEQ_1, TDGROUP, TREES_3, TARSKI, FUNCT_1, NUMBERS,
      MARGREL1, PARTFUN1, PZFMISC1, TREES_4, FUNCT_6, MSUALG_3, MSUALG_6,
      PUA2MSS1, CARD_3, RLTOPSP1, FUNCT_4, REWRITE1, REALSET1, CAT_1, ZFMISC_1,
      NAT_1, MEMBER_1, INSTALG1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1,
      NUMBERS, FINSEQ_1, STRUCT_0, FINSEQ_2, CARD_3, LANG1, TREES_3, TREES_4,
      DTCONSTR, REWRITE1, FUNCT_7, PBOOLE, PZFMISC1, MSUALG_1, PARTFUN1,
      FUNCT_2, PRALG_2, MSUALG_3, PUA2MSS1, MSAFREE, MSATERM, MSUALG_6;
 constructors NAT_1, REWRITE1, PZFMISC1, FUNCT_7, PRALG_2, MSUALG_3, MSATERM,
      PUA2MSS1, MSUALG_6, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, PBOOLE, TREES_3,
      STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSATERM, MSUALG_9, RELSET_1,
      FINSEQ_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, STRUCT_0, FUNCT_1, MSUALG_1, MSUALG_3, PUA2MSS1, MSUALG_6,
      PBOOLE, PZFMISC1;
 theorems ZFMISC_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, FINSEQ_1, TARSKI,
      TREES_4, PBOOLE, MSUALG_1, MSUALG_3, REWRITE1, PRALG_2, PUA2MSS1,
      MSAFREE, MSATERM, EXTENS_1, MSUALG_6, RELSET_1, XBOOLE_0, MSALIMIT,
      PARTFUN1, FINSEQ_2, XTUPLE_0;
 schemes CLASSES1, MSATERM, MSUALG_6, FUNCT_1;

begin :: Preliminaries

theorem Th1:
  for S being non empty non void ManySortedSign for o being
  OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
  being set holds x is ArgumentSeq of Sym(o,V) iff x is Element of Args(o,
  FreeMSA V)
proof
  let S be non empty non void ManySortedSign;
  let o be OperSymbol of S;
  let V be non-empty ManySortedSet of the carrier of S;
  let x be set;
A1: TS DTConMSA V = S-Terms V by MSATERM:def 1;
A2: FreeMSA V = MSAlgebra(#FreeSort V, FreeOper V#) by MSAFREE:def 14;
  hereby
    assume x is ArgumentSeq of Sym(o,V);
    then reconsider p = x as ArgumentSeq of Sym(o,V);
    reconsider p as FinSequence of TS DTConMSA V by MSATERM:def 1;
    Sym(o, V) ==> roots p by MSATERM:21;
    hence x is Element of Args(o, FreeMSA V) by A2,MSAFREE:10;
  end;
  assume x is Element of Args(o, FreeMSA V);
  then reconsider x as Element of Args(o, FreeMSA V);
  rng x c= TS DTConMSA V
  proof
    let y be set;
    assume y in rng x;
    then consider z being set such that
A3: z in dom x and
A4: y = x.z by FUNCT_1:def 3;
    reconsider z as Element of NAT by A3;
A5: (FreeSort V).((the_arity_of o)/.z) = FreeSort(V,(the_arity_of o)/.z)
    by MSAFREE:def 11;
    dom x = dom the_arity_of o by MSUALG_6:2;
    then y in (FreeSort V).((the_arity_of o)/.z) by A2,A3,A4,MSUALG_6:2;
    hence thesis by A5;
  end;
  then reconsider x as FinSequence of TS DTConMSA V by FINSEQ_1:def 4;
  Sym(o, V) ==> roots x by A2,MSAFREE:10;
  hence thesis by A1,MSATERM:21;
end;

registration
  let S be non empty non void ManySortedSign;
  let V be non-empty ManySortedSet of the carrier of S;
  let o be OperSymbol of S;
  cluster -> DTree-yielding for Element of Args(o, FreeMSA V);
  coherence by Th1;
end;

theorem Th2:
  for S being non empty non void ManySortedSign for A1,A2 being
  MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 for o
  being OperSymbol of S st Args(o,A1) <> {} holds Args(o,A2) <> {}
proof
  let S be non void non empty ManySortedSign;
  let A1,A2 be MSAlgebra over S such that
A1: for i be set st i in the carrier of S & (the Sorts of A2).i = {}
  holds (the Sorts of A1).i = {};
  let o be OperSymbol of S;
  assume
A2: Args(o,A1) <> {};
  now
    let i be Element of NAT;
    assume i in dom the_arity_of o;
    then (the Sorts of A1).((the_arity_of o)/.i) <> {} by A2,MSUALG_6:3;
    hence (the Sorts of A2).((the_arity_of o)/.i) <> {} by A1;
  end;
  hence thesis by MSUALG_6:3;
end;

theorem Th3:
  for S being non empty non void ManySortedSign for o being
  OperSymbol of S for V being non-empty ManySortedSet of the carrier of S for x
being Element of Args(o, FreeMSA V) holds Den(o,FreeMSA V).x = [o, the carrier
  of S]-tree x
proof
  let S be non empty non void ManySortedSign;
  let o be OperSymbol of S;
  let V be non-empty ManySortedSet of the carrier of S;
  let x be Element of Args(o, FreeMSA V);
A1: FreeMSA V = MSAlgebra(#FreeSort(V), FreeOper(V)#) by MSAFREE:def 14;
  reconsider p = x as ArgumentSeq of Sym(o,V) by Th1;
A2: Sym(o, V) = [o, the carrier of S] by MSAFREE:def 9;
  p is FinSequence of TS DTConMSA V & Sym(o, V) ==> roots p by MSATERM:21,def 1
;
  then DenOp(o,V).x = [o, the carrier of S]-tree x by A2,MSAFREE:def 12;
  hence thesis by A1,MSAFREE:def 13;
end;

theorem
  for S being non empty non void ManySortedSign for A,B being MSAlgebra
  over S st the MSAlgebra of A = the MSAlgebra of B for o being OperSymbol of S
  holds Den(o,A) = Den(o,B);

theorem Th5:
  for S being non empty non void ManySortedSign for A1,A2,B1,B2
  being MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the
  MSAlgebra of A2 = the MSAlgebra of B2 for f being ManySortedFunction of A1,A2
for g being ManySortedFunction of B1,B2 st f = g for o being OperSymbol of S st
  Args(o,A1) <> {} & Args(o,A2) <> {} for x being Element of Args(o,A1) for y
  being Element of Args(o,B1) st x = y holds f#x = g#y
proof
  let S be non empty non void ManySortedSign;
  let A1,A2,B1,B2 be MSAlgebra over S such that
A1: the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra of A2 =
  the MSAlgebra of B2;
  let f be ManySortedFunction of A1,A2;
  let g be ManySortedFunction of B1,B2 such that
A2: f = g;
  let o be OperSymbol of S such that
A3: Args(o,A1) <> {} & Args(o,A2) <> {};
  let x be Element of Args(o,A1);
  let y be Element of Args(o,B1);
  assume
A4: x = y;
  f#x = (Frege(f*the_arity_of o)).x by A3,MSUALG_3:def 5;
  hence thesis by A1,A2,A3,A4,MSUALG_3:def 5;
end;

theorem
  for S being non empty non void ManySortedSign for A1,A2,B1,B2 being
  MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra
of A2 = the MSAlgebra of B2 & the Sorts of A1 is_transformable_to the Sorts of
  A2 for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 ex h9
  being ManySortedFunction of B1,B2 st h9 = h & h9 is_homomorphism B1,B2
proof
  let S be non empty non void ManySortedSign;
  let A1,A2,B1,B2 be MSAlgebra over S such that
A1: the MSAlgebra of A1 = the MSAlgebra of B1 and
A2: the MSAlgebra of A2 = the MSAlgebra of B2 and
A3: the Sorts of A1 is_transformable_to the Sorts of A2;
  let h be ManySortedFunction of A1,A2 such that
A4: h is_homomorphism A1,A2;
  reconsider h9 = h as ManySortedFunction of B1,B2 by A1,A2;
  take h9;
  thus h9 = h;
  let o be OperSymbol of S;
  assume
A5: Args(o,B1) <> {};
  then
A6: Args(o,B2) <> {} by A1,A2,A3,Th2;
  let x be Element of Args(o,B1);
  reconsider y = x as Element of Args(o,A1) by A1;
  thus (h9.(the_result_sort_of o)).(Den(o,B1).x) = (h.(the_result_sort_of o)).
  (Den(o,A1).y) by A1
    .= Den(o,A2).(h#y) by A1,A4,A5,MSUALG_3:def 7
    .= Den(o,B2).(h9#x) by A1,A2,A5,A6,Th5;
end;

definition
  let S be ManySortedSign;
  attr S is feasible means
  : Def1:
  the carrier of S = {} implies the carrier' of S = {};
end;

theorem Th7:
  for S being ManySortedSign holds S is feasible iff dom the
  ResultSort of S = the carrier' of S
proof
  let S be ManySortedSign;
  hereby
    assume S is feasible;
    then the carrier of S = {} implies the carrier' of S = {} by Def1;
    hence dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
  end;
  assume dom the ResultSort of S = the carrier' of S & the carrier of S = {}
  & the carrier' of S <> {};
  hence contradiction;
end;

registration
  cluster non empty -> feasible for ManySortedSign;
  coherence
  proof
    let S be ManySortedSign;
    assume the carrier of S is non empty & the carrier of S = {};
    hence thesis;
  end;
  cluster void -> feasible for ManySortedSign;
  coherence
  proof
    let S be ManySortedSign;
    assume that
A1: S is void and
    the carrier of S = {};
    thus thesis by A1;
  end;
  cluster empty feasible -> void for ManySortedSign;
  coherence
  proof
    let S be ManySortedSign;
    assume
A2: the carrier of S is empty;
    assume the carrier of S = {} implies the carrier' of S = {};
    hence thesis by A2;
  end;
  cluster non void feasible -> non empty for ManySortedSign;
  coherence;
end;

registration
  cluster non void non empty for ManySortedSign;
  existence
  proof
    set S = the non void non empty ManySortedSign;
    take S;
    thus thesis;
  end;
end;

theorem Th8:
  for S being feasible ManySortedSign holds id the carrier of S, id
  the carrier' of S form_morphism_between S,S
proof
  let S be feasible ManySortedSign;
  per cases;
  suppose
    S is void;
    hence thesis by MSALIMIT:6;
  end;
  suppose
    S is non void;
    then reconsider S as non void feasible ManySortedSign;
    S is non empty;
    hence thesis by PUA2MSS1:28;
  end;
end;

theorem Th9:
  for S1,S2 being ManySortedSign for f,g being Function st f,g
  form_morphism_between S1,S2 holds f is Function of the carrier of S1, the
  carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2
proof
  let S1,S2 be ManySortedSign;
  let f,g be Function;
  assume
A1: f,g form_morphism_between S1,S2;
  then
A2: dom f = the carrier of S1 & rng f c= the carrier of S2 by PUA2MSS1:def 12;
  dom g = the carrier' of S1 & rng g c= the carrier' of S2 by A1,
PUA2MSS1:def 12;
  hence thesis by A2,FUNCT_2:2;
end;

begin :: Subsignature

definition
  let S be feasible ManySortedSign;
  mode Subsignature of S -> ManySortedSign means
    : Def2:
    id the carrier of it, id the carrier' of it form_morphism_between it,S;
  existence
  proof
    take S;
    thus thesis by Th8;
  end;
end;

theorem Th10:
  for S being feasible ManySortedSign, T being Subsignature of S
holds the carrier of T c= the carrier of S & the carrier' of T c= the carrier'
  of S
proof
  let S be feasible ManySortedSign, T be Subsignature of S;
  set g = id the carrier' of T;
  id the carrier of T, g form_morphism_between T,S by Def2;
  then rng id the carrier of T c= the carrier of S & rng id the carrier' of T
  c= the carrier' of S by PUA2MSS1:def 12;
  hence thesis;
end;

registration
  let S be feasible ManySortedSign;
  cluster -> feasible for Subsignature of S;
  coherence
  proof
    let T be Subsignature of S;
    set f = id the carrier of T, g = id the carrier' of T;
A1: dom g = the carrier' of T;
    f, g form_morphism_between T,S by Def2;
    then
A2: f*the ResultSort of T = (the ResultSort of S)*g by PUA2MSS1:def 12;
    assume the carrier of T = {};
    then
A3: {} = (the ResultSort of S)*g by A2;
    the carrier' of S = dom the ResultSort of S & rng g = the carrier' of
    T by Th7;
    hence thesis by A3,A1,Th10,RELAT_1:27,38;
  end;
end;

theorem Th11:
  for S being feasible ManySortedSign, T being Subsignature of S
holds the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity
  of S
proof
  let S be feasible ManySortedSign, T be Subsignature of S;
  set f = id the carrier of T, g = id the carrier' of T;
A1: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;
A2: f, g form_morphism_between T,S by Def2;
A3: now
    let x be set;
A4: rng the Arity of T c= (the carrier of T)* by RELAT_1:def 19;
    assume
A5: x in dom the Arity of T;
    then (the Arity of T).x in rng the Arity of T by FUNCT_1:def 3;
    then reconsider
    p = (the Arity of T).x as Element of (the carrier of T)* by A4;
    g.x = x by A1,A5,FUNCT_1:17;
    then rng p c= the carrier of T & f*p = (the Arity of S).x by A2,A1,A5,
FINSEQ_1:def 4,PUA2MSS1:def 12;
    hence (the Arity of T).x = (the Arity of S).x by RELAT_1:53;
  end;
  the ResultSort of T = f*the ResultSort of T by FUNCT_2:17
    .= (the ResultSort of S)*g by A2,PUA2MSS1:def 12;
  hence the ResultSort of T c= the ResultSort of S by RELAT_1:50;
  dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
  then dom the Arity of T c= dom the Arity of S by A1,Th10;
  hence thesis by A3,GRFUNC_1:2;
end;

theorem Th12:
  for S being feasible ManySortedSign, T being Subsignature of S
holds the Arity of T = (the Arity of S)|the carrier' of T & the ResultSort of T
  = (the ResultSort of S)|the carrier' of T
proof
  let S be feasible ManySortedSign, T be Subsignature of S;
A1: the Arity of T c= the Arity of S by Th11;
  the carrier of T = {} implies the carrier' of T = {} by Def1;
  then
A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def 1;
  dom the Arity of T = the carrier' of T & the ResultSort of T c= the
  ResultSort of S by Th11,FUNCT_2:def 1;
  hence thesis by A2,A1,GRFUNC_1:23;
end;

theorem Th13:
  for S,T being feasible ManySortedSign st the carrier of T c= the
  carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the
  ResultSort of S holds T is Subsignature of S
proof
  let S,T be feasible ManySortedSign;
  assume that
A1: the carrier of T c= the carrier of S and
A2: the Arity of T c= the Arity of S and
A3: the ResultSort of T c= the ResultSort of S;
  set f = id the carrier of T, g = id the carrier' of T;
  thus dom f = the carrier of T & dom g = the carrier' of T;
  thus rng f c= the carrier of S by A1;
A4: dom the Arity of T = the carrier' of T by FUNCT_2:def 1;
  dom the Arity of S = the carrier' of S & rng g = the carrier' of T by
FUNCT_2:def 1;
  hence rng g c= the carrier' of S by A2,A4,GRFUNC_1:2;
A5: dom the ResultSort of T = the carrier' of T by Th7;
  rng the ResultSort of T c= the carrier of T by RELAT_1:def 19;
  hence f*the ResultSort of T = the ResultSort of T by RELAT_1:53
    .= (the ResultSort of S)|the carrier' of T by A3,A5,GRFUNC_1:23
    .= (the ResultSort of S)*g by RELAT_1:65;
  let o be set, p be Function;
  assume that
A6: o in the carrier' of T and
A7: p = (the Arity of T).o;
  reconsider q = p as Element of (the carrier of T)* by A6,A7,FUNCT_2:5;
  rng q c= the carrier of T by FINSEQ_1:def 4;
  hence f*p = p by RELAT_1:53
    .= (the Arity of S).o by A2,A4,A6,A7,GRFUNC_1:2
    .= (the Arity of S).(g.o) by A6,FUNCT_1:17;
end;

theorem
  for S,T being feasible ManySortedSign st the carrier of T c= the
  carrier of S & the Arity of T = (the Arity of S)|the carrier' of T & the
  ResultSort of T = (the ResultSort of S)|the carrier' of T holds T is
  Subsignature of S
proof
  let S,T be feasible ManySortedSign such that
A1: the carrier of T c= the carrier of S;
  assume that
A2: the Arity of T = (the Arity of S)|the carrier' of T and
A3: the ResultSort of T = (the ResultSort of S)|the carrier' of T;
  the Arity of T c= the Arity of S by A2,RELAT_1:59;
  hence thesis by A1,A3,Th13,RELAT_1:59;
end;

theorem Th15:
  for S being feasible ManySortedSign holds S is Subsignature of S
proof
  let S be feasible ManySortedSign;
  thus id the carrier of S, id the carrier' of S form_morphism_between S,S by
Th8;
end;

theorem
  for S1 being feasible ManySortedSign for S2 being Subsignature of S1
  for S3 being Subsignature of S2 holds S3 is Subsignature of S1
proof
  let S1 be feasible ManySortedSign;
  let S2 be Subsignature of S1, S3 be Subsignature of S2;
  rng id the carrier of S3 = the carrier of S3;
  then
A1: (id the carrier of S2)*id the carrier of S3 = id the carrier of S3 by Th10,
RELAT_1:53;
  rng id the carrier' of S3 = the carrier' of S3;
  then
A2: (id the carrier' of S2)*id the carrier' of S3 = id the carrier' of S3 by
Th10,RELAT_1:53;
  id the carrier of S3,id the carrier' of S3 form_morphism_between S3,S2 &
id the carrier of S2,id the carrier' of S2 form_morphism_between S2,S1 by Def2;
  hence id the carrier of S3,id the carrier' of S3 form_morphism_between S3,
  S1 by A1,A2,PUA2MSS1:29;
end;

theorem
  for S1 being feasible ManySortedSign for S2 being Subsignature of S1
st S1 is Subsignature of S2 holds the ManySortedSign of S1 = the ManySortedSign
  of S2
proof
  let S1 be feasible ManySortedSign;
  let S2 be Subsignature of S1;
A1: the carrier of S2 c= the carrier of S1 by Th10;
  assume
A2: S1 is Subsignature of S2;
  then the carrier of S1 c= the carrier of S2 by Th10;
  then
A3: the carrier of S1 = the carrier of S2 by A1,XBOOLE_0:def 10;
A4: the carrier' of S2 c= the carrier' of S1 by Th10;
  the carrier' of S1 c= the carrier' of S2 by A2,Th10;
  then
A5: the carrier' of S1 = the carrier' of S2 by A4,XBOOLE_0:def 10;
A6: the Arity of S2 c= the Arity of S1 by Th11;
A7: the ResultSort of S2 c= the ResultSort of S1 by Th11;
  the ResultSort of S1 c= the ResultSort of S2 by A2,Th11;
  then
A8: the ResultSort of S1 = the ResultSort of S2 by A7,XBOOLE_0:def 10;
  the Arity of S1 c= the Arity of S2 by A2,Th11;
  hence thesis by A6,A3,A5,A8,XBOOLE_0:def 10;
end;

registration
  let S be non empty ManySortedSign;
  cluster non empty for Subsignature of S;
  existence
  proof
    reconsider T = S as Subsignature of S by Th15;
    take T;
    thus thesis;
  end;
end;

registration
  let S be non void feasible ManySortedSign;
  cluster non void for Subsignature of S;
  existence
  proof
    reconsider T = S as Subsignature of S by Th15;
    take T;
    thus thesis;
  end;
end;

theorem
  for S being feasible ManySortedSign, S9 being Subsignature of S for T
being ManySortedSign, f,g being Function st f,g form_morphism_between S,T holds
  f|the carrier of S9, g|the carrier' of S9 form_morphism_between S9,T
proof
  let S be feasible ManySortedSign, S9 be Subsignature of S;
  let T be ManySortedSign, f,g be Function;
A1: g|the carrier' of S9 = g*id the carrier' of S9 by RELAT_1:65;
  id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S &
  f| the carrier of S9 = f*id the carrier of S9 by Def2,RELAT_1:65;
  hence thesis by A1,PUA2MSS1:29;
end;

theorem
  for S being ManySortedSign, T being feasible ManySortedSign for T9
  being Subsignature of T, f,g being Function st f,g form_morphism_between S,T9
  holds f,g form_morphism_between S,T
proof
  let S be ManySortedSign, T be feasible ManySortedSign;
  let T9 be Subsignature of T, f,g be Function such that
A1: f,g form_morphism_between S,T9;
  rng f c= the carrier of T9 by A1,PUA2MSS1:def 12;
  then
A2: (id the carrier of T9)*f = f by RELAT_1:53;
  rng g c= the carrier' of T9 by A1,PUA2MSS1:def 12;
  then
A3: (id the carrier' of T9)*g = g by RELAT_1:53;
  id the carrier of T9, id the carrier' of T9 form_morphism_between T9,T
  by Def2;
  hence thesis by A1,A2,A3,PUA2MSS1:29;
end;

theorem
  for S being ManySortedSign, T being feasible ManySortedSign for T9
being Subsignature of T, f,g being Function st f,g form_morphism_between S,T &
  rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g
  form_morphism_between S,T9
proof
  let S be ManySortedSign, T be feasible ManySortedSign;
  let T9 be Subsignature of T, f,g be Function;
  assume that
A1: dom f = the carrier of S and
A2: dom g = the carrier' of S and
  rng f c= the carrier of T and
  rng g c= the carrier' of T and
A3: f*the ResultSort of S = (the ResultSort of T)*g and
A4: for o being set, p being Function st o in the carrier' of S & p = (
  the Arity of S).o holds f*p = (the Arity of T).(g.o) and
A5: rng f c= the carrier of T9 and
A6: rng g c= the carrier' of T9;
  thus dom f = the carrier of S & dom g = the carrier' of S by A1,A2;
  thus rng f c= the carrier of T9 & rng g c= the carrier' of T9 by A5,A6;
  thus f*the ResultSort of S = (the ResultSort of T)*((id the carrier' of T9)*
  g) by A3,A6,RELAT_1:53
    .= (the ResultSort of T)*(id the carrier' of T9)*g by RELAT_1:36
    .= ((the ResultSort of T)|the carrier' of T9)*g by RELAT_1:65
    .= (the ResultSort of T9)*g by Th12;
  let o be set, p be Function;
  assume that
A7: o in the carrier' of S and
A8: p = (the Arity of S).o;
A9: the Arity of T9 c= the Arity of T & dom the Arity of T9 = the carrier'
  of T9 by Th11,FUNCT_2:def 1;
  g.o in rng g by A2,A7,FUNCT_1:def 3;
  then (the Arity of T9).(g.o) = (the Arity of T).(g.o) by A6,A9,GRFUNC_1:2;
  hence thesis by A4,A7,A8;
end;

begin :: Signature reduct

definition
  let S1,S2 be non empty ManySortedSign;
  let A be MSAlgebra over S2;
  let f,g be Function such that
B1: f,g form_morphism_between S1,S2;
  func A|(S1,f,g) -> strict MSAlgebra over S1 means
  : Def3:
  the Sorts of it =
  (the Sorts of A)*f & the Charact of it = (the Charact of A)*g;
  existence
  proof
    dom f = the carrier of S1 & rng f c= the carrier of S2 by B1,
PUA2MSS1:def 12;
    then reconsider
    f9 = f as Function of the carrier of S1,the carrier of S2 by FUNCT_2:def 1
,RELSET_1:4;
A1: rng g c= the carrier' of S2 by B1,PUA2MSS1:def 12;
A2: dom g = the carrier' of S1 by B1,PUA2MSS1:def 12;
    then reconsider
    g9 = g as Function of the carrier' of S1,the carrier' of S2 by A1,FUNCT_2:2
;
    dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;
    then dom ((the Charact of A)*g9) = the carrier' of S1 by A2,A1,RELAT_1:27;
    then reconsider
    C = (the Charact of A)*g9 as ManySortedSet of the carrier' of
    S1 by PARTFUN1:def 2;
    C is ManySortedFunction of ((the Sorts of A)*f9)#*the Arity of S1, (
    the Sorts of A)*f9*the ResultSort of S1
    proof
      let o be set;
      assume
A3:   o in the carrier' of S1;
      then reconsider
      p1 = (the Arity of S1).o as Element of (the carrier of S1 )*
      by FUNCT_2:5;
A4:   g.o in rng g by A2,A3,FUNCT_1:def 3;
      then reconsider
      p2 = (the Arity of S2).(g.o) as Element of (the carrier of S2
      )* by A1,FUNCT_2:5;
      reconsider o as OperSymbol of S1 by A3;
A5:   C.o = (the Charact of A).(g9.o) by A1,A3,A4,FUNCT_2:15;
      (the Sorts of A)*f9*the ResultSort of S1 = (the Sorts of A)*(f9*the
      ResultSort of S1) by RELAT_1:36
        .= (the Sorts of A)*((the ResultSort of S2)*g) by B1,PUA2MSS1:def 12
        .= (the Sorts of A)*(the ResultSort of S2)*g by RELAT_1:36;
      then
A6:   ((the Sorts of A)*f9*the ResultSort of S1).o = ((the Sorts of A)*(
      the ResultSort of S2)).(g9.o) by A1,A3,A4,FUNCT_2:15;
A7:   (the Sorts of A)*f9*p1 = (the Sorts of A)*(f9*p1) by RELAT_1:36
        .= (the Sorts of A)*p2 by B1,A3,PUA2MSS1:def 12;
      (((the Sorts of A)*f9)#*the Arity of S1).o = ((the Sorts of A)*f9)#
      .p1 by A3,FUNCT_2:15
        .= product((the Sorts of A)*f9*p1) by FINSEQ_2:def 5
        .= (the Sorts of A)#.p2 by A7,FINSEQ_2:def 5
        .= ((the Sorts of A)#*the Arity of S2).(g9.o) by A1,A4,FUNCT_2:15;
      hence thesis by A1,A4,A6,A5,PBOOLE:def 15;
    end;
    then reconsider
    C as ManySortedFunction of ((the Sorts of A)*f9)#*the Arity of
    S1, (the Sorts of A)*f9*the ResultSort of S1;
    take MSAlgebra(#(the Sorts of A)*f9, C#);
    thus thesis;
  end;
  correctness;
end;

definition
  let S2,S1 be non empty ManySortedSign;
  let A be MSAlgebra over S2;
  func A|S1 -> strict MSAlgebra over S1 equals
  A|(S1, id the carrier of S1, id
  the carrier' of S1);
  correctness;
end;

theorem
  for S1,S2 being non empty ManySortedSign for A,B being MSAlgebra over
  S2 st the MSAlgebra of A = the MSAlgebra of B for f,g being Function st f,g
  form_morphism_between S1,S2 holds A|(S1,f,g) = B|(S1,f,g)
proof
  let S1,S2 be non empty ManySortedSign;
  let A,B be MSAlgebra over S2 such that
A1: the MSAlgebra of A = the MSAlgebra of B;
  let f,g be Function;
  assume
A2: f,g form_morphism_between S1,S2;
  then
  the Sorts of A|(S1,f,g) = (the Sorts of A)*f & the Charact of A|(S1,f,g)
  = ( the Charact of A)*g by Def3;
  hence thesis by A1,A2,Def3;
end;

theorem Th22:
  for S1,S2 being non empty ManySortedSign for A being non-empty
  MSAlgebra over S2 for f,g being Function st f,g form_morphism_between S1,S2
  holds A|(S1,f,g) is non-empty
proof
  let S1,S2 be non empty ManySortedSign;
  let A be non-empty MSAlgebra over S2;
  let f,g be Function;
  assume f,g form_morphism_between S1,S2;
  then the Sorts of (A|(S1,f,g)) = (the Sorts of A)*f by Def3;
  hence the Sorts of (A|(S1,f,g)) is non-empty;
end;

registration
  let S2 be non empty ManySortedSign;
  let S1 be non empty Subsignature of S2;
  let A be non-empty MSAlgebra over S2;
  cluster A|S1 -> non-empty;
  coherence
  proof
    id the carrier of S1, id the carrier' of S1 form_morphism_between S1,
    S2 by Def2;
    hence thesis by Th22;
  end;
end;

theorem Th23:
  for S1,S2 being non void non empty ManySortedSign for f,g being
  Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1 holds Den(o1,
  A|(S1,f,g)) = Den(o2,A)
proof
  let S1,S2 be non void non empty ManySortedSign;
  let f,g be Function;
  assume
A1: f,g form_morphism_between S1,S2;
  then reconsider
  g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
  let A be MSAlgebra over S2;
  let o1 be OperSymbol of S1, o2 be OperSymbol of S2;
  assume o2 = g.o1;
  then (the Charact of A).o2 = ((the Charact of A)*g9).o1 by FUNCT_2:15
    .= (the Charact of A|(S1,f,g)).o1 by A1,Def3;
  hence thesis;
end;

theorem Th24:
  for S1,S2 being non void non empty ManySortedSign for f,g being
  Function st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 for
o1 being OperSymbol of S1, o2 being OperSymbol of S2 st o2 = g.o1 holds Args(o2
  ,A) = Args(o1,A|(S1,f,g)) & Result(o1,A|(S1,f,g)) = Result(o2,A)
proof
  let S1,S2 be non void non empty ManySortedSign;
  let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
A2: dom f = the carrier of S1 by A1,PUA2MSS1:def 12;
  let A be MSAlgebra over S2;
  let o1 be OperSymbol of S1, o2 be OperSymbol of S2;
  assume
A3: o2 = g.o1;
  thus Args(o2,A) = product ((the Sorts of A)*the_arity_of o2) by PRALG_2:3
    .= product ((the Sorts of A)*(f*the_arity_of o1)) by A1,A3,PUA2MSS1:def 12
    .= product ((the Sorts of A)*f*the_arity_of o1) by RELAT_1:36
    .= product ((the Sorts of A|(S1,f,g))*the_arity_of o1) by A1,Def3
    .= Args(o1,A|(S1,f,g)) by PRALG_2:3;
  dom g = the carrier' of S1 by A1,PUA2MSS1:def 12;
  then the_result_sort_of o2 = ((the ResultSort of S2)*g).o1 by A3,FUNCT_1:13
    .= (f*the ResultSort of S1).o1 by A1,PUA2MSS1:def 12
    .= f.the_result_sort_of o1 by FUNCT_2:15;
  hence Result(o2,A) = (the Sorts of A).(f.the_result_sort_of o1) by PRALG_2:3
    .= ((the Sorts of A)*f).the_result_sort_of o1 by A2,FUNCT_1:13
    .= (the Sorts of A|(S1,f,g)).the_result_sort_of o1 by A1,Def3
    .= Result(o1,A|(S1,f,g)) by PRALG_2:3;
end;

theorem Th25:
  for S being non empty ManySortedSign for A being MSAlgebra over
  S holds A|(S, id the carrier of S, id the carrier' of S) = the MSAlgebra of A
proof
  let S be non empty ManySortedSign;
  let A be MSAlgebra over S;
  set f = id the carrier of S, g = id the carrier' of S;
  dom the Charact of A = the carrier' of S by PARTFUN1:def 2;
  then
A1: the Charact of the MSAlgebra of A = (the Charact of A)*g by RELAT_1:52;
  dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
  then
A2: the Sorts of the MSAlgebra of A = (the Sorts of A)*f by RELAT_1:52;
  f,g form_morphism_between S,S by Th8;
  hence thesis by A2,A1,Def3;
end;

theorem
  for S being non empty ManySortedSign for A being MSAlgebra over S
  holds A|S = the MSAlgebra of A by Th25;

theorem Th27:
  for S1,S2,S3 being non empty ManySortedSign for f1,g1 being
Function st f1,g1 form_morphism_between S1,S2 for f2,g2 being Function st f2,g2
form_morphism_between S2,S3 for A being MSAlgebra over S3 holds A|(S1,f2*f1,g2*
  g1) = (A|(S2,f2,g2))|(S1,f1,g1)
proof
  let S1,S2,S3 be non empty ManySortedSign;
  let f1,g1 be Function such that
A1: f1,g1 form_morphism_between S1,S2;
  let f2,g2 be Function such that
A2: f2,g2 form_morphism_between S2,S3;
A3: f2*f1, g2*g1 form_morphism_between S1,S3 by A1,A2,PUA2MSS1:29;
  let A be MSAlgebra over S3;
A4: the Charact of (A|(S2,f2,g2))|(S1,f1,g1) = (the Charact of A|(S2,f2,g2))
  *g1 by A1,Def3
    .= (the Charact of A)*g2*g1 by A2,Def3
    .= (the Charact of A)*(g2*g1) by RELAT_1:36;
  the Sorts of (A|(S2,f2,g2))|(S1,f1,g1) = (the Sorts of A|(S2,f2,g2))*f1
  by A1,Def3
    .= (the Sorts of A)*f2*f1 by A2,Def3
    .= (the Sorts of A)*(f2*f1) by RELAT_1:36;
  hence thesis by A3,A4,Def3;
end;

theorem
  for S1 being non empty feasible ManySortedSign for S2 being non empty
  Subsignature of S1 for S3 being non empty Subsignature of S2 for A being
  MSAlgebra over S1 holds A|S3 = (A|S2)|S3
proof
  let S1 be non empty feasible ManySortedSign;
  let S2 be non empty Subsignature of S1;
  let S3 be non empty Subsignature of S2;
  let A be MSAlgebra over S1;
  set f1 = id the carrier of S2, g1 = id the carrier' of S2;
  set f2 = id the carrier of S3, g2 = id the carrier' of S3;
  rng f2 = the carrier of S3;
  then
A1: f1*f2 = f2 by Th10,RELAT_1:53;
  rng g2 = the carrier' of S3;
  then
A2: g1*g2 = g2 by Th10,RELAT_1:53;
  f1,g1 form_morphism_between S2,S1 & f2,g2 form_morphism_between S3,S2 by Def2
;
  hence thesis by A1,A2,Th27;
end;

theorem Th29:
  for S1,S2 being non empty ManySortedSign for f being Function of
  the carrier of S1, the carrier of S2 for g being Function st f,g
  form_morphism_between S1,S2 for A1,A2 being MSAlgebra over S2 for h being
  ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h*f is
  ManySortedFunction of the Sorts of A1|(S1,f,g), the Sorts of A2|(S1,f,g)
proof
  let S1,S2 be non empty ManySortedSign;
  let f be Function of the carrier of S1, the carrier of S2;
  let g be Function such that
A1: f,g form_morphism_between S1,S2;
  let A1,A2 be MSAlgebra over S2;
  let h be ManySortedFunction of the Sorts of A1,the Sorts of A2;
  set B1 = A1|(S1,f,g), B2 = A2|(S1,f,g);
  let x be set;
  assume x in the carrier of S1;
  then reconsider s = x as SortSymbol of S1;
  reconsider fs = f.s as SortSymbol of S2;
A2: (h*f).s = h.fs & (the Sorts of A1).fs = ((the Sorts of A1)*f).s by
FUNCT_2:15;
A3: (the Sorts of A2).fs = ((the Sorts of A2)*f).s by FUNCT_2:15;
  (the Sorts of A1)*f = the Sorts of B1 & (the Sorts of A2)*f = the Sorts
  of B2 by A1,Def3;
  hence thesis by A2,A3;
end;

theorem
  for S1 being non empty ManySortedSign for S2 being non empty
  Subsignature of S1 for A1,A2 being MSAlgebra over S1 for h being
  ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h|the carrier of
  S2 is ManySortedFunction of the Sorts of A1|S2, the Sorts of A2|S2
proof
  let S1 be non empty ManySortedSign;
  let S2 be non empty Subsignature of S1;
  set f = id the carrier of S2, g = id the carrier' of S2;
  let A1,A2 be MSAlgebra over S1;
  let h be ManySortedFunction of the Sorts of A1, the Sorts of A2;
A1: f,g form_morphism_between S2,S1 by Def2;
  then reconsider f as Function of the carrier of S2, the carrier of S1 by Th9
;
  h*f is ManySortedFunction of the Sorts of A1|(S2,f,g), the Sorts of A2|(
  S2,f,g) by A1,Th29;
  hence thesis by RELAT_1:65;
end;

theorem Th31:
  for S1,S2 being non empty ManySortedSign for f,g being Function
st f,g form_morphism_between S1,S2 for A being MSAlgebra over S2 holds (id the
  Sorts of A)*f = id the Sorts of A|(S1,f,g)
proof
  let S1,S2 be non empty ManySortedSign;
  let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
  dom f = the carrier of S1 & rng f c= the carrier of S2 by A1,PUA2MSS1:def 12;
  then reconsider f as Function of the carrier of S1, the carrier of S2 by
FUNCT_2:def 1,RELSET_1:4;
  let A be MSAlgebra over S2;
  now
    let i be set;
    assume i in the carrier of S1;
    then reconsider s = i as SortSymbol of S1;
    thus ((id the Sorts of A)*f).i = (id the Sorts of A).(f.s) by FUNCT_2:15
      .= id ((the Sorts of A).(f.s)) by MSUALG_3:def 1
      .= id (((the Sorts of A)*f).s) by FUNCT_2:15
      .= id ((the Sorts of A|(S1,f,g)).s) by A1,Def3
      .= (id the Sorts of A|(S1,f,g)).i by MSUALG_3:def 1;
  end;
  hence thesis by PBOOLE:3;
end;

theorem
  for S1 being non empty ManySortedSign for S2 being non empty
Subsignature of S1 for A being MSAlgebra over S1 holds (id the Sorts of A)|the
  carrier of S2 = id the Sorts of A|S2
proof
  let S1 be non empty ManySortedSign;
  let S2 be non empty Subsignature of S1;
  set f = id the carrier of S2, g = id the carrier' of S2;
  let A be MSAlgebra over S1;
  f,g form_morphism_between S2,S1 by Def2;
  then (id the Sorts of A)*f = id the Sorts of A|S2 by Th31;
  hence thesis by RELAT_1:65;
end;

theorem Th33:
  for S1,S2 being non void non empty ManySortedSign for f,g being
Function st f,g form_morphism_between S1,S2 for A,B being MSAlgebra over S2 for
h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of A|(S1,f,g
),B|(S1,f,g) st h1 = h2*f for o1 being OperSymbol of S1, o2 being OperSymbol of
  S2 st o2 = g.o1 & Args(o2,A) <> {} & Args(o2,B) <> {} for x2 being Element of
Args(o2,A) for x1 being Element of Args(o1,A|(S1,f,g)) st x2 = x1 holds h1#x1 =
  h2#x2
proof
  let S1,S2 be non void non empty ManySortedSign;
  let f,g be Function such that
A1: f,g form_morphism_between S1,S2;
  let A2,B2 be MSAlgebra over S2;
  set A1 = A2|(S1,f,g), B1 = B2|(S1,f,g);
  let h2 be ManySortedFunction of A2,B2;
  let h1 be ManySortedFunction of A1,B1 such that
A2: h1 = h2*f;
  let o1 be OperSymbol of S1, o2 be OperSymbol of S2 such that
A3: o2 = g.o1;
  assume that
A4: Args(o2,A2) <> {} and
A5: Args(o2,B2) <> {};
  let x2 be Element of Args(o2,A2);
  let x1 be Element of Args(o1,A1);
  assume
A6: x2 = x1;
  then reconsider f1 = x1, f2 = x2, g2 = h2#x2 as Function by A4,A5,MSUALG_6:1;
A7: Args(o2,A2) = Args(o1,A1) by A1,A3,Th24;
  then
A8: dom f1 = dom the_arity_of o1 by A4,MSUALG_3:6;
A9: dom f2 = dom the_arity_of o2 by A4,MSUALG_3:6;
A10: now
    let i be Nat;
    assume
A11: i in dom f1;
    dom f = the carrier of S1 by A1,PUA2MSS1:def 12;
    then h1.((the_arity_of o1)/.i) = h2.(f.((the_arity_of o1)/.i)) by A2,
FUNCT_1:13
      .= h2.(f.((the_arity_of o1).i)) by A8,A11,PARTFUN1:def 6
      .= h2.((f*the_arity_of o1).i) by A8,A11,FUNCT_1:13
      .= h2.((the_arity_of o2).i) by A1,A3,PUA2MSS1:def 12
      .= h2.((the_arity_of o2)/.i) by A6,A9,A11,PARTFUN1:def 6;
    hence g2.i = (h1.((the_arity_of o1)/.i)).(f1.i) by A4,A5,A6,A11,MSUALG_3:24
;
  end;
  Args(o2,B2) = Args(o1,B1) by A1,A3,Th24;
  hence thesis by A4,A5,A7,A10,MSUALG_3:24;
end;

theorem Th34:
  for S,S9 being non empty non void ManySortedSign for A1,A2 being
  MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 for h
  being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 for f being
  Function of the carrier of S9, the carrier of S for g being Function st f,g
form_morphism_between S9,S ex h9 being ManySortedFunction of A1|(S9,f,g), A2|(
  S9,f,g) st h9 = h*f & h9 is_homomorphism A1|(S9,f,g), A2|(S9,f,g)
proof
  let S,S9 be non empty non void ManySortedSign;
  let A1,A2 be MSAlgebra over S such that
A1: the Sorts of A1 is_transformable_to the Sorts of A2;
  let h be ManySortedFunction of A1,A2 such that
A2: h is_homomorphism A1,A2;
  let f be Function of the carrier of S9, the carrier of S;
  let g be Function such that
A3: f,g form_morphism_between S9,S;
A4: dom g = the carrier' of S9 & rng g c= the carrier' of S by A3,
PUA2MSS1:def 12;
  set B1 = A1|(S9,f,g), B2 = A2|(S9,f,g);
  reconsider g as Function of the carrier' of S9, the carrier' of S by A4,
FUNCT_2:def 1,RELSET_1:4;
A5: f*the ResultSort of S9 = (the ResultSort of S)*g by A3,PUA2MSS1:def 12;
  reconsider h9 = h*f as ManySortedFunction of B1,B2 by A3,Th29;
  take h9;
  thus h9 = h*f;
  let o be OperSymbol of S9;
  set go = g.o;
  assume
A6: Args(o,B1) <> {};
  let x be Element of Args(o,B1);
  reconsider y = x as Element of Args(go,A1) by A3,Th24;
A7: h9.the_result_sort_of o = h.(f.the_result_sort_of o) by FUNCT_2:15
    .= h.(((the ResultSort of S)*g).o) by A5,FUNCT_2:15
    .= h.the_result_sort_of go by FUNCT_2:15;
A8: Den(o,B1) = Den(go,A1) & Den(o,B2) = Den(go,A2) by A3,Th23;
A9: Args(o,B1) = Args(g.o,A1) by A3,Th24;
A10: Args(o,B2) = Args(g.o,A2) by A3,Th24;
  then Args(o,B2) <> {} by A1,A6,A9,Th2;
  then h9#x = h#y by A3,A6,A9,A10,Th33;
  hence thesis by A2,A6,A9,A8,A7,MSUALG_3:def 7;
end;

theorem
  for S being non void feasible ManySortedSign for S9 being non void
  Subsignature of S for A1,A2 being MSAlgebra over S st the Sorts of A1
is_transformable_to the Sorts of A2 for h being ManySortedFunction of A1,A2 st
h is_homomorphism A1,A2 ex h9 being ManySortedFunction of A1|S9, A2|S9 st h9 =
  h|the carrier of S9 & h9 is_homomorphism A1|S9, A2|S9
proof
  let S be non void feasible ManySortedSign;
  let S9 be non void Subsignature of S;
  let A1,A2 be MSAlgebra over S such that
A1: the Sorts of A1 is_transformable_to the Sorts of A2;
  set f = id the carrier of S9, g = id the carrier' of S9;
A2: f,g form_morphism_between S9,S by Def2;
  then reconsider f as Function of the carrier of S9, the carrier of S by Th9;
  let h be ManySortedFunction of A1,A2;
  assume h is_homomorphism A1,A2;
  then consider
  h9 being ManySortedFunction of A1|(S9,f,g), A2|(S9,f,g) such that
A3: h9 = h*f and
A4: h9 is_homomorphism A1|(S9,f,g), A2|(S9,f,g) by A1,A2,Th34;
  consider k being ManySortedFunction of A1|S9, A2|S9 such that
A5: k = h9 and
  k is_homomorphism A1|S9, A2|S9 by A4;
  take k;
  thus thesis by A3,A4,A5,RELAT_1:65;
end;

theorem Th36:
  for S,S9 being non empty non void ManySortedSign for A being
  non-empty MSAlgebra over S for f being Function of the carrier of S9, the
carrier of S for g being Function st f,g form_morphism_between S9,S for B being
non-empty MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9,
t being Function st t is_e.translation_of B, s1, s2 holds t is_e.translation_of
  A, f.s1, f.s2
proof
  let S,S9 be non empty non void ManySortedSign;
  let A be non-empty MSAlgebra over S;
  let f be Function of the carrier of S9, the carrier of S;
  let g be Function such that
A1: f,g form_morphism_between S9,S;
A2: dom g = the carrier' of S9 & rng g c= the carrier' of S by A1,
PUA2MSS1:def 12;
  let B be non-empty MSAlgebra over S9 such that
A3: B = A|(S9,f,g);
  reconsider g as Function of the carrier' of S9, the carrier' of S by A2,
FUNCT_2:def 1,RELSET_1:4;
  let s1,s2 be SortSymbol of S9, t be Function;
  given o being OperSymbol of S9 such that
A4: the_result_sort_of o = s2 and
A5: ex i being Element of NAT st i in dom the_arity_of o & (the_arity_of
  o)/.i = s1 & ex a being Function st a in Args(o,B) & t = transl(o,i,a,B);
A6: f*the_arity_of o = the_arity_of (g.o) by A1,PUA2MSS1:def 12;
  take g.o;
  f*the ResultSort of S9 = (the ResultSort of S)*g by A1,PUA2MSS1:def 12;
  hence the_result_sort_of (g.o) = (f*the ResultSort of S9).o by FUNCT_2:15
    .= f.s2 by A4,FUNCT_2:15;
  consider i being (Element of NAT), a being Function such that
A7: i in dom the_arity_of o and
A8: (the_arity_of o)/.i = s1 and
A9: a in Args(o,B) and
A10: t = transl(o,i,a,B) by A5;
  take i;
  rng the_arity_of o c= the carrier of S9 & dom f = the carrier of S9 by
FINSEQ_1:def 4,FUNCT_2:def 1;
  hence i in dom the_arity_of (g.o) by A7,A6,RELAT_1:27;
  hence
A11: (the_arity_of (g.o))/.i = (the_arity_of (g.o)).i by PARTFUN1:def 6
    .= f.((the_arity_of o).i) by A7,A6,FUNCT_1:13
    .= f.s1 by A7,A8,PARTFUN1:def 6;
  then
A12: dom transl(g.o, i, a, A) = (the Sorts of A).(f.s1) by MSUALG_6:def 4;
A13: the Sorts of B = (the Sorts of A)*f by A1,A3,Def3;
  then
A14: (the Sorts of B).s1 = (the Sorts of A).(f.s1) by FUNCT_2:15;
A15: now
    let x be set;
    assume x in (the Sorts of B).s1;
    then
    t.x = Den(o,B).(a+*(i,x)) & transl(g.o,i,a,A).x = Den(g.o,A).(a+*(i,x
    ) ) by A8,A10,A11,A14,MSUALG_6:def 4;
    hence t.x = transl(g.o,i,a,A).x by A1,A3,Th23;
  end;
  take a;
  thus a in Args(g.o,A) by A1,A3,A9,Th24;
  dom t = (the Sorts of B).s1 by A8,A10,MSUALG_6:def 4;
  hence thesis by A12,A13,A15,FUNCT_1:2,FUNCT_2:15;
end;

Lm1: for S,S9 being non empty non void ManySortedSign for A being non-empty
MSAlgebra over S for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S for B being non-empty
MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9 st
TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2 & for
t being Translation of B, s1, s2 holds t is Translation of A, f.s1, f.s2
proof
  let S,S9 be non void non empty ManySortedSign;
  let A be non-empty MSAlgebra over S;
  let f be Function of the carrier of S9, the carrier of S;
  let g be Function such that
A1: f,g form_morphism_between S9,S;
  defpred P[set, SortSymbol of S9, SortSymbol of S9] means TranslationRel S
  reduces f.$2, f.$3 & $1 is Translation of A, f.$2,f.$3;
  let B be non-empty MSAlgebra over S9 such that
A2: B = A|(S9,f,g);
A3: for s1,s2,s3 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2
  for t being Translation of B,s1,s2 st P[t,s1,s2] for h being Function st h
  is_e.translation_of B,s2,s3 holds P[h*t,s1,s3]
  proof
    let s1,s2,s3 be SortSymbol of S9 such that
    TranslationRel S9 reduces s1,s2;
    let t be Translation of B,s1,s2 such that
A4: P[t,s1,s2];
    let h be Function;
    assume
A5: h is_e.translation_of B,s2,s3;
    then [f.s2, f.s3] in TranslationRel S by A1,A2,Th36,MSUALG_6:12;
    then
A6: TranslationRel S reduces f.s2, f.s3 by REWRITE1:15;
    h is_e.translation_of A, f.s2, f.s3 by A1,A2,A5,Th36;
    hence thesis by A4,A6,MSUALG_6:19,REWRITE1:16;
  end;
  let s1,s2 be SortSymbol of S9;
  assume
A7: TranslationRel S9 reduces s1,s2;
A8: for s being SortSymbol of S9 holds P[id ((the Sorts of B).s),s,s]
  proof
    let s be SortSymbol of S9;
    thus TranslationRel S reduces f.s, f.s by REWRITE1:12;
    the Sorts of B = (the Sorts of A)*f by A1,A2,Def3;
    then (the Sorts of B).s = (the Sorts of A).(f.s) by FUNCT_2:15;
    hence thesis by MSUALG_6:16;
  end;
  for s1,s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 for
  t being Translation of B,s1,s2 holds P[t,s1,s2] from MSUALG_6:sch 1(A8,A3);
  hence thesis by A7;
end;

theorem
  for S,S9 being non empty non void ManySortedSign for f being Function
  of the carrier of S9, the carrier of S for g being Function st f,g
  form_morphism_between S9,S for s1,s2 being SortSymbol of S9 st TranslationRel
  S9 reduces s1,s2 holds TranslationRel S reduces f.s1, f.s2
proof
  let S,S9 be non empty non void ManySortedSign;
  set A = the non-empty MSAlgebra over S;
  let f be Function of the carrier of S9, the carrier of S;
  let g be Function;
  assume
A1: f,g form_morphism_between S9,S;
  then A|(S9,f,g) is non-empty MSAlgebra over S9 by Th22;
  hence thesis by A1,Lm1;
end;

theorem
  for S,S9 being non void non empty ManySortedSign for A being non-empty
  MSAlgebra over S for f being Function of the carrier of S9, the carrier of S
  for g being Function st f,g form_morphism_between S9,S for B being non-empty
  MSAlgebra over S9 st B = A|(S9,f,g) for s1,s2 being SortSymbol of S9 st
TranslationRel S9 reduces s1,s2 for t being Translation of B, s1, s2 holds t is
  Translation of A, f.s1, f.s2 by Lm1;

begin :: Translating homomorphism

scheme
  GenFuncEx{S() -> non empty non void ManySortedSign, A() -> non-empty
MSAlgebra over S(), X() -> non-empty ManySortedSet of the carrier of S(), F(set
  ,set) -> set}: ex h being ManySortedFunction of FreeMSA X(), A() st h
  is_homomorphism FreeMSA X(), A() & for s being SortSymbol of S() for x being
  Element of X().s holds h.s.root-tree [x,s] = F(x,s)
provided
A1: for s being SortSymbol of S() for x being Element of X().s holds F(x
,s) in (the Sorts of A()).s
proof
  defpred P[set,set] means ex f being Function of (FreeGen X()).$1, (the Sorts
of A()).$1 st $2 = f & for x being Element of X().$1 holds f.root-tree [x,$1] =
  F(x,$1);
A2: for a being set st a in the carrier of S() ex y being set st P[a,y]
  proof
    let a be set;
    assume a in the carrier of S();
    then reconsider s = a as SortSymbol of S();
    defpred P[set,set] means ex x being Element of X().s st $1 = root-tree [x,
    s] & $2 = F(x,s);
A3: (FreeGen X()).s = FreeGen(s, X()) by MSAFREE:def 16;
A4: for y being set st y in (FreeGen X()).s ex z being set st z in (the
    Sorts of A()).s & P[y,z]
    proof
      let y be set;
      assume y in (FreeGen X()).s;
      then consider a be set such that
A5:   a in X().s and
A6:   y = root-tree [a,s] by A3,MSAFREE:def 15;
      reconsider a as Element of X().s by A5;
      take z = F(a,s);
      thus z in (the Sorts of A()).s by A1;
      take a;
      thus thesis by A6;
    end;
    consider f being Function such that
A7: dom f = (FreeGen X()).s & rng f c= (the Sorts of A()).s and
A8: for y being set st y in (FreeGen X()).s holds P[y,f.y] from
    FUNCT_1:sch 5(A4);
    reconsider f as Function of (FreeGen X()).a, (the Sorts of A()).a by A7,
FUNCT_2:2;
    take y = f, f;
    thus y = f;
    let x be Element of X().a;
    root-tree [x,s] in (FreeGen X()).s by A3,MSAFREE:def 15;
    then consider z being Element of X().s such that
A9: root-tree [x,s] = root-tree [z,s] and
A10: f.root-tree [x,s] = F(z,s) by A8;
    [x,s] = [z,s] by A9,TREES_4:4;
    hence thesis by A10,XTUPLE_0:1;
  end;
  consider h being Function such that
A11: dom h = the carrier of S() and
A12: for a being set st a in the carrier of S() holds P[a,h.a] from
  CLASSES1:sch 1(A2);
  reconsider h as ManySortedSet of the carrier of S() by A11,PARTFUN1:def 2
,RELAT_1:def 18;
  h is ManySortedFunction of FreeGen X(), the Sorts of A()
  proof
    let a be set;
    assume a in the carrier of S();
    then
    ex f being Function of (FreeGen X()).a, (the Sorts of A()).a st h.a =
    f & for x being Element of X().a holds f.root-tree [x,a] = F(x,a) by A12;
    hence thesis;
  end;
  then reconsider h as ManySortedFunction of FreeGen X(), the Sorts of A();
  consider H being ManySortedFunction of FreeMSA X(), A() such that
A13: H is_homomorphism FreeMSA X(), A() and
A14: H||FreeGen X() = h by MSAFREE:def 5;
  take H;
  thus H is_homomorphism FreeMSA X(), A() by A13;
  let s be SortSymbol of S(), x be Element of X().s;
A15: ex f being Function of (FreeGen X()).s, (the Sorts of A()).s st h.s = f
  & for x being Element of X().s holds f.root-tree [x,s] = F(x,s) by A12;
  reconsider t = root-tree [x,s] as Term of S(), X() by MSATERM:4;
  (FreeGen X()).s = FreeGen(s,X()) by MSAFREE:def 16;
  then
A16: t in (FreeGen X()).s by MSAFREE:def 15;
  h.s = (H.s)|((FreeGen X()).s) by A14,MSAFREE:def 1;
  then H.s.root-tree [x,s] = h.s.root-tree [x,s] by A16,FUNCT_1:49;
  hence thesis by A15;
end;

theorem Th39:
  for I being set, A,B being ManySortedSet of I for C being
ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st
i in I for f,g being Function st f = F.i & g = (F||C).i for x being set st x in
  C.i holds g.x = f.x
proof
  let I be set, A,B be ManySortedSet of I;
  let C be ManySortedSubset of A;
  let F be ManySortedFunction of A,B;
  let i be set;
  assume
A1: i in I;
  then reconsider Fi = F.i as Function of A.i, B.i by PBOOLE:def 15;
  let f,g be Function;
  assume that
A2: f = F.i and
A3: g = (F||C).i;
  let x be set;
  g = Fi|(C.i) by A1,A3,MSAFREE:def 1;
  hence thesis by A2,FUNCT_1:49;
end;

registration
  let S be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S;
  cluster FreeGen X -> non-empty;
  coherence;
end;

definition
  let S1,S2 be non empty non void ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S2;
  let f be Function of the carrier of S1, the carrier of S2;
  let g be Function such that
B1: f,g form_morphism_between S1,S2;
  func hom(f,g,X,S1,S2) -> ManySortedFunction of FreeMSA(X*f), (FreeMSA X)|(S1
  ,f,g) means
  : Def5:
  it is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) & for
s being SortSymbol of S1, x being Element of (X*f).s holds it.s.root-tree [x,s]
  = root-tree [x,f.s];
  existence
  proof
    set A = (FreeMSA X)|(S1,f,g);
    the Sorts of A = (the Sorts of FreeMSA X)*f by B1,Def3;
    then reconsider A as non-empty MSAlgebra over S1 by MSUALG_1:def 3;
    deffunc F(set,set)=root-tree [$1,f.$2];
A1: now
      let s be SortSymbol of S1, x be Element of (X*f).s;
      reconsider fs = f.s as SortSymbol of S2;
      reconsider y = x as Element of X.fs by FUNCT_2:15;
      reconsider t = root-tree [y,fs] as Term of S2,X by MSATERM:4;
      the_sort_of t = fs by MSATERM:14;
      then t in FreeSort(X,fs) by MSATERM:def 5;
      then
A2:   t in (FreeSort X).fs by MSAFREE:def 11;
      FreeMSA X = MSAlgebra(#FreeSort X,FreeOper X#) & the Sorts of A = (
      the Sorts of FreeMSA X)*f by B1,Def3,MSAFREE:def 14;
      hence F(x,s) in (the Sorts of A).s by A2,FUNCT_2:15;
    end;
    consider H being ManySortedFunction of FreeMSA(X*f), A such that
A3: H is_homomorphism FreeMSA(X*f), A & for s being SortSymbol of S1
    for x being Element of (X*f).s holds H.s.root-tree [x,s] = F(x,s) from
    GenFuncEx(A1);
    reconsider G = H as ManySortedFunction of FreeMSA(X*f), (FreeMSA X)|(S1,f,
    g);
    take G;
    thus thesis by A3;
  end;
  uniqueness
  proof
    reconsider A1 = (FreeMSA X)|(S1,f,g) as non-empty MSAlgebra over S1 by B1
,Th22;
    let G1,G2 be ManySortedFunction of the Sorts of FreeMSA(X*f), the Sorts of
    (FreeMSA X)|(S1,f,g) such that
A4: G1 is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) and
A5: for s being SortSymbol of S1, x being Element of (X*f).s holds G1
    .s.root-tree [x,s] = root-tree [x,f.s] and
A6: G2 is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) and
A7: for s being SortSymbol of S1, x being Element of (X*f).s holds G2
    .s.root-tree [x,s] = root-tree [x,f.s];
    set H1 = G1, H2 = G2;
A8: now
      let x be set;
      assume x in the carrier of S1;
      then reconsider s = x as SortSymbol of S1;
      reconsider g1 = (H1||FreeGen (X*f)).s, g2 = (H2||FreeGen (X*f)).s as
      Function of (FreeGen (X*f)).s, (the Sorts of A1).s;
      now
        let z be Element of (FreeGen (X*f)).s;
        FreeGen(s,X*f) = (FreeGen(X*f)).s by MSAFREE:def 16;
        then consider a being set such that
A9:    a in (X*f).s and
A10:    z = root-tree [a,s] by MSAFREE:def 15;
        reconsider a as Element of (X*f).s by A9;
        thus g1.z = H1.s.z by Th39
          .= root-tree [a,f.s] by A5,A10
          .= H2.s.z by A7,A10
          .= g2.z by Th39;
      end;
      hence (H1||FreeGen (X*f)).x = (H2||FreeGen (X*f)).x by FUNCT_2:63;
    end;
    A1 = (FreeMSA X)|(S1,f,g);
    hence thesis by A4,A6,A8,EXTENS_1:14,PBOOLE:3;
  end;
end;

theorem Th40:
  for S1,S2 being non void non empty ManySortedSign for X being
  non-empty ManySortedSet of the carrier of S2 for f being Function of the
  carrier of S1, the carrier of S2 for g being Function st f,g
  form_morphism_between S1,S2 for o being OperSymbol of S1, p being Element of
Args(o,FreeMSA(X*f)) for q being FinSequence st q = hom(f,g,X,S1,S2)#p holds (
  hom(f,g,X,S1,S2).the_result_sort_of o).([o,the carrier of S1]-tree p) = [g.o,
  the carrier of S2]-tree q
proof
  let S1,S2 be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S2;
  let f be Function of the carrier of S1, the carrier of S2;
  let g be Function;
  set F = hom(f,g,X,S1,S2);
  assume
A1: f,g form_morphism_between S1,S2;
  then reconsider
  h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
  let o be OperSymbol of S1, p be Element of Args(o,FreeMSA(X*f));
  let q be FinSequence;
  assume
A2: q = F#p;
  then
A3: q is Element of Args(h.o,FreeMSA X) by A1,Th24;
  F is_homomorphism FreeMSA(X*f), (FreeMSA X)|(S1,f,g) by A1,Def5;
  then
  (F.(the_result_sort_of o)).(Den(o,FreeMSA(X*f)).p) = Den(o,(FreeMSA X)|(
  S1,f,g)).q by A2,MSUALG_3:def 7;
  hence (F.the_result_sort_of o).([o,the carrier of S1]-tree p) = Den(o,(
  FreeMSA X)|(S1,f,g)).q by Th3
    .= Den(h.o, FreeMSA X).q by A1,Th23
    .= [g.o, the carrier of S2]-tree q by A3,Th3;
end;

theorem Th41:
  for S1,S2 being non void non empty ManySortedSign for X being
  non-empty ManySortedSet of the carrier of S2 for f being Function of the
  carrier of S1, the carrier of S2 for g being Function st f,g
form_morphism_between S1,S2 for t being Term of S1, X*f holds (hom(f,g,X,S1,S2)
  .the_sort_of t).t is CompoundTerm of S2, X iff t is CompoundTerm of S1, X*f
proof
  let S1,S2 be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S2;
  let f be Function of the carrier of S1, the carrier of S2;
  let g be Function;
  assume
A1: f,g form_morphism_between S1,S2;
  then reconsider
  h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
  let t be Term of S1, X*f;
  hereby
    assume (hom(f,g,X,S1,S2).the_sort_of t).t is CompoundTerm of S2, X;
    then reconsider
    w = (hom(f,g,X,S1,S2).the_sort_of t).t as CompoundTerm of S2,X;
    assume t is not CompoundTerm of S1, X*f;
    then not t.{} in [:the carrier' of S1, {the carrier of S1}:] by
MSATERM:def 6;
    then consider
    s being SortSymbol of S1, v being Element of (X*f).s such that
A2: t.{} = [v,s] by MSATERM:2;
    t = root-tree [v,s] by A2,MSATERM:5;
    then hom(f,g,X,S1,S2).s.t = root-tree [v,f.s] & the_sort_of t = s by A1
,Def5,MSATERM:14;
    then w.{} in [:the carrier' of S2, {the carrier of S2}:] & w.{} = [v,f.s]
    by MSATERM:def 6,TREES_4:3;
    then
A3: f.s = the carrier of S2 by ZFMISC_1:106;
    f.s in the carrier of S2;
    hence contradiction by A3;
  end;
  assume t is CompoundTerm of S1, X*f;
  then reconsider t as CompoundTerm of S1, X*f;
  t.{} in [:the carrier' of S1, {the carrier of S1}:] by MSATERM:def 6;
  then consider o,r being set such that
A4: o in the carrier' of S1 and
A5: r in {the carrier of S1} and
A6: t.{} = [o,r] by ZFMISC_1:def 2;
  reconsider o as OperSymbol of S1 by A4;
  r = the carrier of S1 by A5,TARSKI:def 1;
  then consider a being ArgumentSeq of Sym(o,X*f) such that
A7: t = [o,the carrier of S1]-tree a by A6,MSATERM:10;
  reconsider a as Element of Args(o, FreeMSA(X*f)) by Th1;
  reconsider b = hom(f,g,X,S1,S2)#a as Element of Args(h.o, FreeMSA X) by A1
,Th24;
A8: (hom(f,g,X,S1,S2).the_result_sort_of o).([o,the carrier of S1]-tree a)
  = [g.o,the carrier of S2]-tree b by A1,Th40;
  t.{} = [o,the carrier of S1] by A7,TREES_4:def 4;
  then
A9: the_sort_of t = the_result_sort_of o by MSATERM:17;
  reconsider b as ArgumentSeq of Sym(h.o, X) by Th1;
  Sym(h.o, X)-tree b = [h.o,the carrier of S2]-tree b by MSAFREE:def 9;
  then reconsider T = [h.o,the carrier of S2]-tree b as Term of S2, X;
  T.{} = [g.o,the carrier of S2] & [h.o,the carrier of S2] in [:the
  carrier' of S2, {the carrier of S2 } :] by TREES_4:def 4,ZFMISC_1:106;
  hence thesis by A7,A9,A8,MSATERM:def 6;
end;

theorem
  for S1,S2 being non void non empty ManySortedSign for X being
  non-empty ManySortedSet of the carrier of S2 for f being Function of the
  carrier of S1, the carrier of S2 for g being one-to-one Function st f,g
form_morphism_between S1,S2 holds hom(f,g,X,S1,S2) is_monomorphism FreeMSA(X*f)
  , (FreeMSA X)|(S1,f,g)
proof
  let S1,S2 be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S2;
  let f be Function of the carrier of S1, the carrier of S2;
  let g be one-to-one Function;
  set A = (FreeMSA X)|(S1,f,g);
  set H = hom(f,g,X,S1,S2);
  defpred P[set] means ex t1 being Term of S1, X*f st t1 = $1 & for t2 being
Term of S1, X*f st the_sort_of t1 = the_sort_of t2 & (H.the_sort_of t1).t1 = (H
  .the_sort_of t1).t2 holds t1 = t2;
A1: FreeMSA (X*f) = MSAlgebra(#FreeSort(X*f), FreeOper(X*f)#) by MSAFREE:def 14
;
  assume
A2: f,g form_morphism_between S1,S2;
  then reconsider
  h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
  reconsider B = A as non-empty MSAlgebra over S1 by A2,Th22;
  reconsider H9 = H as ManySortedFunction of FreeMSA(X*f), B;
A3: for o being OperSymbol of S1, p being ArgumentSeq of Sym(o,X*f) st for
  t being Term of S1,X*f st t in rng p holds P[t] holds P[[o,the carrier of S1]
  -tree p]
  proof
    let o be OperSymbol of S1, p be ArgumentSeq of Sym(o,X*f) such that
A4: for t being Term of S1,X*f st t in rng p holds P[t];
A5: dom p = dom the_arity_of o by MSATERM:22;
    reconsider a = p as Element of Args(o, FreeMSA(X*f)) by Th1;
A6: [h.o,the carrier of S2] in [:the carrier' of S2, {the carrier of S2}
    :] by ZFMISC_1:106;
    reconsider q = H#a as Element of Args(h.o, FreeMSA X) by A2,Th24;
    take t1 = Sym(o,X*f)-tree p;
    thus
A7: t1 = [o,the carrier of S1]-tree p by MSAFREE:def 9;
    reconsider b = q as ArgumentSeq of Sym(h.o, X) by Th1;
    let t2 be Term of S1, X*f such that
A8: the_sort_of t1 = the_sort_of t2 & (H.the_sort_of t1).t1 = (H.
    the_sort_of t1) .t2;
    the_sort_of t1 = the_result_sort_of o by MSATERM:20;
    then
A9: (H.the_sort_of t1).t1 = [g.o,the carrier of S2]-tree q by A2,A7,Th40;
    (Sym(h.o, X)-tree b).{} = Sym(h.o, X) & Sym(h.o, X) = [h.o,the
    carrier of S2 ] by MSAFREE:def 9,TREES_4:def 4;
    then [h.o, the carrier of S2]-tree b is CompoundTerm of S2, X by A6,
MSATERM:def 6;
    then t2 is CompoundTerm of S1, X*f by A2,A8,A9,Th41;
    then t2.{} in [:the carrier' of S1, {the carrier of S1}:] by MSATERM:def 6;
    then consider o9,s9 being set such that
A10: o9 in the carrier' of S1 and
A11: s9 in {the carrier of S1} & t2.{} = [o9, s9] by ZFMISC_1:def 2;
    reconsider o9 as OperSymbol of S1 by A10;
A12: t2.{} = [o9, the carrier of S1] by A11,TARSKI:def 1;
    then consider r being ArgumentSeq of Sym(o9, X*f) such that
A13: t2 = [o9, the carrier of S1]-tree r by MSATERM:10;
    reconsider c = r as Element of Args(o9, FreeMSA(X*f)) by Th1;
    reconsider R = H#c as Element of Args(h.o9, FreeMSA X) by A2,Th24;
    the_result_sort_of o9 = the_sort_of t2 by A12,MSATERM:17;
    then
A14: (H.the_sort_of t1).t1 = [g.o9,the carrier of S2]-tree R by A2,A8,A13,Th40;
    then [g.o9, the carrier of S2] = [g.o,the carrier of S2] by A9,TREES_4:15;
    then h.o = h.o9 by XTUPLE_0:1;
    then
A15: o = o9 by FUNCT_2:19;
    then
A16: dom r = dom the_arity_of o by MSATERM:22;
A17: q = R by A9,A14,TREES_4:15;
    now
      let i be Nat;
A18:  R = H9#c;
      assume
A19:  i in dom the_arity_of o;
      then reconsider w1 = p.i, w2 = r.i as Term of S1,X*f by A5,A16,MSATERM:22
;
A20:  the_sort_of w1 = (the_arity_of o)/.i by A5,A19,MSATERM:23;
      q = H9#a;
      then q.i = (H.the_sort_of w1).w1 by A5,A19,A20,MSUALG_3:def 6;
      then
A21:  (H.the_sort_of w1).w1 = (H.the_sort_of w1).w2 by A17,A15,A16,A19,A20,A18,
MSUALG_3:def 6;
      w1 in rng p by A5,A19,FUNCT_1:def 3;
      then
A22:  P[w1] by A4;
      the_sort_of w2 = (the_arity_of o)/.i by A15,A16,A19,MSATERM:23;
      hence p.i = r.i by A22,A20,A21;
    end;
    hence thesis by A7,A13,A15,A5,A16,FINSEQ_1:13;
  end;
  thus H is_homomorphism FreeMSA(X*f), A by A2,Def5;
  let i be set, h be Function;
  assume i in dom H;
  then reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;
  assume
A23: H.i = h;
  then
A24: dom h = dom (H9.s) .= (FreeSort(X*f)).s by A1,FUNCT_2:def 1
    .= FreeSort(X*f,s) by MSAFREE:def 11;
  let x,y be set;
  assume
A25: x in dom h & y in dom h;
  FreeSort(X*f,s) c= S1-Terms (X*f) by MSATERM:12;
  then reconsider t1 = x, t2 = y as Term of S1, X*f by A24,A25;
A26: for s being SortSymbol of S1, v being Element of (X*f).s holds P[
  root-tree [v,s]]
  proof
    let s be SortSymbol of S1, v be Element of (X*f).s;
    reconsider t1 = root-tree [v,s] as Term of S1, X*f by MSATERM:4;
    take t1;
    thus t1 = root-tree [v,s];
    let t2 be Term of S1, X*f such that
A27: the_sort_of t1 = the_sort_of t2 and
A28: (H.the_sort_of t1).t1 = (H.the_sort_of t1).t2;
A29: the_sort_of t1 = s by MSATERM:14;
A30: H.s.root-tree [v,s] = root-tree [v,f.s] by A2,Def5;
    now
      assume t2.{} in [:the carrier' of S1,{the carrier of S1}:];
      then t2 is CompoundTerm of S1, X*f by MSATERM:def 6;
      then (root-tree [v,f.s]).{} = [v,f.s] & root-tree [v,f.s] is
      CompoundTerm of S2, X by A2,A27,A28,A30,A29,Th41,TREES_4:3;
      then [v,f.s] in [:the carrier' of S2, {the carrier of S2}:] by
MSATERM:def 6;
      then
A31:  f.s = the carrier of S2 by ZFMISC_1:106;
      f.s in the carrier of S2;
      hence contradiction by A31;
    end;
    then consider
    s2 being SortSymbol of S1, v2 being Element of (X*f).s2 such that
A32: t2.{} = [v2,s2] by MSATERM:2;
A33: t2 = root-tree [v2,s2] by A32,MSATERM:5;
    then
A34: s = s2 by A27,A29,MSATERM:14;
    then H.s.t2 = root-tree [v2,f.s] by A2,A33,Def5;
    then [v,f.s] = [v2,f.s] by A28,A30,A29,TREES_4:4;
    hence thesis by A33,A34,XTUPLE_0:1;
  end;
  for t being Term of S1,X*f holds P[t] from MSATERM:sch 1(A26,A3);
  then
A35: P[t1];
  the_sort_of t1 = s & the_sort_of t2 = s by A24,A25,MSATERM:def 5;
  hence thesis by A23,A35;
end;

theorem
  for S being non void non empty ManySortedSign for X being non-empty
  ManySortedSet of the carrier of S holds hom(id the carrier of S, id the
  carrier' of S, X, S, S) = id the Sorts of FreeMSA X
proof
  let S be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S;
  set f = id the carrier of S;
  set h = hom(f, id the carrier' of S, X, S, S);
  set I = id the Sorts of FreeMSA X, g = id the carrier' of S;
A1: f, g form_morphism_between S,S by PUA2MSS1:28;
  dom X = the carrier of S by PARTFUN1:def 2;
  then
A2: X*f = X by RELAT_1:52;
A3: (FreeMSA X)|(S,f,g) = FreeMSA X by Th25;
A4: now
    let i be set;
    assume i in the carrier of S;
    then reconsider s = i as SortSymbol of S;
    FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
    then
A5: (FreeGen X).s c= (the Sorts of FreeMSA X).s by PBOOLE:def 2;
    then (I.s)|((FreeGen X).s) is Function of (FreeGen X).s, (the Sorts of
    FreeMSA X).s by FUNCT_2:32;
    then
A6: dom ((I.s)|((FreeGen X).s)) = (FreeGen X).s by FUNCT_2:def 1;
A7: now
      let a be set;
      assume
A8:   a in (FreeGen X).s;
      then reconsider b = a as Element of FreeMSA X,s by A5;
      b in FreeGen(s,X) by A8,MSAFREE:def 16;
      then consider x being set such that
A9:   x in X.s and
A10:  b = root-tree [x,s] by MSAFREE:def 15;
      thus ((I.s)|((FreeGen X).s)).a = I.s.b by A8,FUNCT_1:49
        .= (id ((the Sorts of FreeMSA X).s)).b by MSUALG_3:def 1
        .= b by FUNCT_1:18
        .= root-tree [x,f.s] by A10,FUNCT_1:18
        .= h.s.b by A1,A2,A9,A10,Def5
        .= ((h.s)|((FreeGen X).s)).a by A8,FUNCT_1:49;
    end;
    (h.s)|((FreeGen X).s) is Function of (FreeGen X).s, (the Sorts of
    FreeMSA X).s by A2,A3,A5,FUNCT_2:32;
    then
A11: dom ((h.s)|((FreeGen X).s)) = (FreeGen X).s by FUNCT_2:def 1;
    (I||FreeGen X).s = (I.s)|((FreeGen X).s) & (h||FreeGen (X*f)).s = (h.s
    )|(( FreeGen (X*f)).s) by MSAFREE:def 1;
    hence (I||FreeGen X).i = (h||FreeGen (X*f)).i by A2,A6,A11,A7,FUNCT_1:2;
  end;
  I is_homomorphism FreeMSA X, FreeMSA X & h is_homomorphism FreeMSA (X*f)
  , ( FreeMSA X)|(S,f,g) by A1,Def5,MSUALG_3:9;
  hence thesis by A2,A3,A4,EXTENS_1:19,PBOOLE:3;
end;

theorem
  for S1,S2,S3 being non void non empty ManySortedSign for X being
  non-empty ManySortedSet of the carrier of S3 for f1 being Function of the
  carrier of S1, the carrier of S2 for g1 being Function st f1,g1
  form_morphism_between S1,S2 for f2 being Function of the carrier of S2, the
carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds
  hom(f2*f1,g2*g1,X,S1,S3) = (hom(f2,g2,X,S2,S3)*f1)**hom(f1,g1,X*f2,S1,S2)
proof
  let S1,S2,S3 be non void non empty ManySortedSign;
  let X be non-empty ManySortedSet of the carrier of S3;
  let f1 be Function of the carrier of S1, the carrier of S2;
  let g1 be Function such that
A1: f1,g1 form_morphism_between S1,S2;
  let f2 be Function of the carrier of S2, the carrier of S3;
  let g2 be Function;
  set f = f2*f1, g = g2*g1;
  assume
A2: f2,g2 form_morphism_between S2,S3;
  then reconsider
  Af = (FreeMSA X)|(S1,f,g), Af1 = (FreeMSA(X*f2))|(S1,f1,g1) as
  non-empty MSAlgebra over S1 by A1,Th22,PUA2MSS1:29;
A3: hom(f2,g2,X,S2,S3) is_homomorphism FreeMSA(X*f2), (FreeMSA X)|(S2,f2,g2)
  by A2,Def5;
A4: the Sorts of FreeMSA(X*f2) is_transformable_to the Sorts of (FreeMSA X)|
  (S2,f2,g2)
  proof
    let i be set;
    assume i in the carrier of S2;
    then reconsider s = i as SortSymbol of S2;
    (the Sorts of (FreeMSA X)|(S2,f2,g2)).s = ((the Sorts of FreeMSA X)*f2
    ).s by A2,Def3;
    hence thesis;
  end;
  (FreeMSA X)|(S1,f,g) = ((FreeMSA X)|(S2,f2,g2))|(S1,f1,g1) by A1,A2,Th27;
  then consider hf1 being ManySortedFunction of Af1, Af such that
A5: hf1 = hom(f2,g2,X,S2,S3)*f1 and
A6: hf1 is_homomorphism Af1, Af by A1,A3,A4,Th34;
  reconsider hh = hom(f1,g1,X*f2,S1,S2) as ManySortedFunction of FreeMSA(X*f),
  Af1 by RELAT_1:36;
  reconsider hf1h = hf1**hh as ManySortedFunction of FreeMSA(X*f), (FreeMSA X)
  |(S1,f,g);
A7: X*f = X*f2*f1 by RELAT_1:36;
A8: now
    let s be SortSymbol of S1, x be Element of (X*f).s;
    reconsider t = root-tree [x,s] as Term of S1, X*f by MSATERM:4;
A9: FreeMSA (X*f) = MSAlgebra(#FreeSort (X*f), FreeOper (X*f)#) by
MSAFREE:def 14;
    the_sort_of t = s & (FreeSort (X*f)).s = FreeSort(X*f,s) by MSAFREE:def 11
,MSATERM:14;
    then
A10: root-tree [x,s] in (the Sorts of FreeMSA(X*f)).s by A9,MSATERM:def 5;
A11: (X*f).s = (X*f2).(f1.s) by A7,FUNCT_2:15;
    hf1h.s.root-tree [x,s] = ((hf1.s)*(hom(f1,g1,X*f2,S1,S2).s)).
    root-tree [x,s] by MSUALG_3:2
      .= (hf1.s).(hom(f1,g1,X*f2,S1,S2).s.root-tree [x,s]) by A7,A10,FUNCT_2:15
      .= (hf1.s).root-tree [x,f1.s] by A1,A7,Def5;
    hence
    hf1h.s.root-tree [x,s] = (hom(f2,g2,X,S2,S3).(f1.s)).root-tree [x,f1.
    s] by A5,FUNCT_2:15
      .= root-tree [x,f2.(f1.s)] by A2,A11,Def5
      .= root-tree [x,f.s] by FUNCT_2:15;
  end;
A12: f, g form_morphism_between S1,S3 by A1,A2,PUA2MSS1:29;
  hom(f1,g1,X*f2,S1,S2) is_homomorphism FreeMSA(X*f2*f1), (FreeMSA (X*f2))
  |(S1,f1,g1) by A1,Def5;
  then hf1**hh is_homomorphism FreeMSA(X*f), Af by A6,A7,MSUALG_3:10;
  hence thesis by A12,A5,A8,Def5;
end;