:: On the Group of Automorphisms of Universal Algebra & Many
:: Sorted Algebra
::  by Artur Korni{\l}owicz
::
:: Received December 13, 1994
:: Copyright (c) 1994 Association of Mizar Users

environ

 vocabularies UNIALG_1, FUNCT_1, GROUP_6, ALG_1, RELAT_1, FRAENKEL, FUNCT_2,
      BINOP_1, REALSET1, GROUP_1, PBOOLE, NATTRA_1, BOOLE, FUNCOP_1, PRALG_1,
      MSUALG_3, ZF_REFLE, AMI_1, MSUALG_1, CARD_3, MSUHOM_1, CQC_SIM1,
      WELLORD1, AUTALG_1, CAT_1, ARYTM, ALGSTR_0, VECTSP_1, SGRAPH1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, NUMBERS, FUNCOP_1, STRUCT_0, ALGSTR_0, FINSEQ_1, BINOP_1,
      FRAENKEL, PBOOLE, GROUP_1, GROUP_6, CARD_3, PZFMISC1, UNIALG_1, UNIALG_2,
      ALG_1, MSUALG_1, MSUALG_3, MSUHOM_1;
 constructors BINOP_1, CARD_3, PRE_CIRC, PZFMISC1, GROUP_6, ALG_1, MSUALG_3,
      MSUHOM_1;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
      FRAENKEL, PBOOLE, STRUCT_0, MSUALG_1, ALGSTR_0;
 requirements BOOLE, SUBSET;
 definitions ALG_1, FRAENKEL, GROUP_1, GROUP_6, MSUALG_3, TARSKI, XBOOLE_0,
      PZFMISC1, FUNCOP_1, ALGSTR_0, FUNCT_2;
 theorems ALG_1, BINOP_1, CARD_3, FUNCOP_1, FUNCT_1, FUNCT_2, GROUP_1, GROUP_6,
      MSUALG_1, MSUALG_3, MSUHOM_1, PBOOLE, TARSKI, ZFMISC_1, RELAT_1,
      RELSET_1, XBOOLE_0, XBOOLE_1, PZFMISC1;
 schemes BINOP_1, FUNCT_1, XBOOLE_0;

begin

:: On the Group of Automorphisms of Universal Algebra

reserve UA for Universal_Algebra,
  f, g for Function of UA, UA;

theorem Th1:
  id the carrier of UA is_isomorphism UA, UA
proof
  set I = id the carrier of UA;
  thus I is_monomorphism UA, UA
  proof
    thus I is_homomorphism UA, UA by ALG_1:6;
    thus I is one-to-one;
  end;
  thus I is_epimorphism UA, UA
  proof
    thus I is_homomorphism UA, UA by ALG_1:6;
    thus rng I = the carrier of UA by RELAT_1:71;
  end;
end;

definition
  let UA;
  func UAAut UA -> FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
  means
  :Def1:
  (for f be Element of it holds f is Function of UA, UA) &
  for h be Function of UA, UA holds h in it iff h is_isomorphism UA, UA;
  existence
  proof
    set F = {x where x is Element of Funcs (the carrier of UA,
    the carrier of UA): x is_isomorphism UA, UA};
A1: id the carrier of UA in F
    proof
      set I = id the carrier of UA;
A2:   I in Funcs (the carrier of UA, the carrier of UA) by FUNCT_2:11;
      I is_isomorphism UA, UA by Th1;
      hence thesis by A2;
    end;
    reconsider F as set;
    F is functional
    proof
      let q be set;
      assume q in F;
      then consider x be Element of Funcs (the carrier of UA, the carrier of UA
      ) such that
A3:   q = x & x is_isomorphism UA, UA;
      thus thesis by A3;
    end;
    then reconsider F as functional non empty set by A1;
    F is FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
    proof
      let a be Element of F;
      a in F;
      then consider x be Element of Funcs (the carrier of UA, the carrier of UA
      ) such that
A4:   a = x & x is_isomorphism UA, UA;
      thus thesis by A4;
    end;
    then reconsider F as FUNCTION_DOMAIN of the carrier of UA, the carrier of
    UA;
    take F;
    thus for f be Element of F holds f is Function of UA, UA;
    let h be Function of UA, UA;
    thus h in F implies h is_isomorphism UA, UA
    proof
      assume h in F;
      then ex f be Element of Funcs (the carrier of UA, the carrier of UA)
      st f = h & f is_isomorphism UA, UA;
      hence h is_isomorphism UA, UA;
    end;
    assume
A5: h is_isomorphism UA, UA;
    h is Element of Funcs (the carrier of UA, the carrier of UA)
    by FUNCT_2:11;
    hence h in F by A5;
  end;
  uniqueness
  proof
    let F1, F2 be FUNCTION_DOMAIN of the carrier of UA, the carrier of UA
    such that
A6: ( for f be Element of F1 holds f is Function of UA, UA ) &
    for h be Function of UA, UA holds h in F1 iff h is_isomorphism UA, UA and
A7: ( for f be Element of F2 holds f is Function of UA, UA ) &
    for h be Function of UA, UA holds h in F2 iff h is_isomorphism UA, UA;
A8: F1 c= F2
    proof
      let q be set;
      assume
A9:   q in F1;
      then reconsider h1 = q as Function of UA, UA by A6;
      h1 is_isomorphism UA, UA by A6,A9;
      hence q in F2 by A7;
    end;
    F2 c= F1
    proof
      let q be set;
      assume
A10:  q in F2;
      then reconsider h1 = q as Function of UA, UA by A7;
      h1 is_isomorphism UA, UA by A7,A10;
      hence q in F1 by A6;
    end;
    hence F1 = F2 by A8,XBOOLE_0:def 10;
  end;
end;

theorem
  UAAut UA c= Funcs (the carrier of UA, the carrier of UA)
proof
  let q be set;
  assume q in UAAut UA;
  then consider f be Element of UAAut UA such that
A1: f = q;
  thus thesis by A1,FUNCT_2:12;
end;

canceled;

theorem Th4:
  id the carrier of UA in UAAut UA
proof
  id the carrier of UA is_isomorphism UA, UA by Th1;
  hence thesis by Def1;
end;

theorem
  for f, g st f is Element of UAAut UA & g = f" holds g is_isomorphism UA, UA
proof
  let f, g;
  assume
A1: f is Element of UAAut UA & g = f";
  then f is_isomorphism UA, UA by Def1;
  hence thesis by A1,ALG_1:11;
end;

Lm1: for f st f is_isomorphism UA, UA holds f" is Function of UA, UA
proof
  let f;
  assume
A1: f is_isomorphism UA, UA;
  then
A2: (f is one-to-one) by ALG_1:8;
  (f is_epimorphism UA, UA) by A1,ALG_1:def 4;
  then rng f = the carrier of UA by ALG_1:def 3;
  hence thesis by A2,FUNCT_2:31;
end;

theorem Th6:
  for f be Element of UAAut UA holds f" in UAAut UA
proof
  let f be Element of UAAut UA;
A1: f is_isomorphism UA, UA by Def1;
  then f" is Function of UA, UA by Lm1;
  then consider ff be Function of UA, UA such that
A2: ff = f";
  ff is_isomorphism UA, UA by A1,A2,ALG_1:11;
  hence thesis by A2,Def1;
end;

theorem Th7:
  for f1, f2 be Element of UAAut UA holds f1 * f2 in UAAut UA
proof
  let f1, f2 be Element of UAAut UA;
  (f1 is_isomorphism UA, UA) & (f2 is_isomorphism UA, UA) by Def1;
  then f1 * f2 is_isomorphism UA, UA by ALG_1:12;
  hence thesis by Def1;
end;

definition
  let UA;
  func UAAutComp UA -> BinOp of UAAut UA means
  :Def2:
  for x, y be Element of UAAut UA holds it.(x, y) = y * x;
  existence
  proof
    defpred P[Element of UAAut UA,Element of UAAut UA,set] means $3 = $2 * $1;
A1: for x, y be Element of UAAut UA ex m be Element of UAAut UA st P[x,y,m]
    proof
      let x, y be Element of UAAut UA;
      reconsider xx = x, yy = y as Function of UA, UA;
      reconsider m = yy * xx as Element of UAAut UA by Th7;
      take m;
      thus thesis;
    end;
    thus ex IT being BinOp of UAAut UA st
    for x, y be Element of UAAut UA holds P[x,y,IT.(x, y)] from BINOP_1:sch 3
    (A1);
  end;
  uniqueness
  proof
    let b1, b2 be BinOp of UAAut UA such that
A2: for x, y be Element of UAAut UA holds b1.(x, y) = y * x and
A3: for x, y be Element of UAAut UA holds b2.(x, y) = y * x;
    for x, y be Element of UAAut UA holds b1.(x, y) = b2.(x, y)
    proof
      let x, y be Element of UAAut UA;
      thus b1.(x, y) = y * x by A2
        .= b2.(x, y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let UA;
  func UAAutGroup UA -> Group equals

  multMagma (# UAAut UA, UAAutComp UA #);
  coherence
  proof
    set H = multMagma (# UAAut UA, UAAutComp UA #);
    H is associative Group-like
    proof
      thus for f, g, h be Element of H holds (f * g) * h = f * (g * h)
      proof
        let f, g, h be Element of H;
        reconsider A = f, B = g, C = h as Element of UAAut UA;
A1:     f * g = B * A by Def2;
A2:     g * h = C * B by Def2;
        thus (f * g) * h = C * (B * A) by A1,Def2
          .= (C * B) * A by RELAT_1:55
          .= f * (g * h) by A2,Def2;
      end; thus
      ex e be Element of H st for h be Element of H holds
      h * e = h & e * h = h & ex g be Element of H st h * g = e & g * h = e
      proof
        reconsider e = id the carrier of UA as Element of H by Th4;
        take e;
        let h be Element of H;
        consider A be Element of UAAut UA such that
A3:     A = h;
        h * e = (id the carrier of UA) * A by A3,Def2
          .= A by FUNCT_2:23;
        hence h * e = h by A3;
        e * h = A * (id the carrier of UA) by A3,Def2
          .= A by FUNCT_2:23;
        hence e * h = h by A3;
        reconsider g = A" as Element of H by Th6;
        take g;
A4:     A is_isomorphism UA, UA by Def1;
        then
A5:     (A is one-to-one) by ALG_1:8;
        (A is_epimorphism UA, UA) by A4,ALG_1:def 4;
        then
A6:     rng A = the carrier of UA by ALG_1:def 3;
        thus h * g = A" * A by A3,Def2
          .= e by A5,A6,FUNCT_2:35;
        thus g * h = A * A" by A3,Def2
          .= e by A5,A6,FUNCT_2:35;
      end;
    end;
    hence thesis;
  end;
end;

registration
  let UA;
  cluster UAAutGroup UA -> strict;
  coherence;
end;

Lm2: for f be Element of UAAut UA holds dom f = rng f &
dom f = the carrier of UA
proof
  let f be Element of UAAut UA;
  f is_isomorphism UA, UA by Def1;
  then (dom f = the carrier of UA) & (rng f = the carrier of UA) by ALG_1:9;
  hence thesis;
end;

theorem
  for x, y be Element of UAAutGroup UA
  for f, g be Element of UAAut UA st x = f & y = g holds x * y = g * f by Def2;

theorem Th9:
  id the carrier of UA = 1_UAAutGroup UA
proof
  reconsider g = id the carrier of UA as Element of UAAutGroup UA by Th4;
  consider g1 be Function of the carrier of UA, the carrier of UA such that
A1: g1 = g;
  consider f be Element of UAAutGroup UA;
  f is Element of UAAut UA;
  then consider f1 be Function of the carrier of UA, the carrier of UA such
  that
A2: f1 = f;
  g * f = f1 * g1 by A1,A2,Def2
    .= f by A1,A2,FUNCT_2:23;
  hence thesis by GROUP_1:15;
end;

theorem
  for f be Element of UAAut UA
  for g be Element of UAAutGroup UA st f = g holds f" = g"
proof
  let f be Element of UAAut UA;
  let g be Element of UAAutGroup UA;
  assume
A1: f = g;
  consider g1 be Element of UAAut UA such that
A2: g1 = g";
A3: rng f = dom f by Lm2
    .= the carrier of UA by Lm2;
  f is_isomorphism UA, UA by Def1;
  then f is_monomorphism UA, UA by ALG_1:def 4;
  then
A4: f is one-to-one by ALG_1:def 2;
  g1 * f = g * g" by A1,A2,Def2;
  then g1 * f = 1_UAAutGroup UA by GROUP_1:def 6;
  then g1 * f = id the carrier of UA by Th9;
  hence thesis by A2,A3,A4,FUNCT_2:36;
end;

begin

:: Some properties of Many Sorted Functions

reserve I for set,
  A, B, C for ManySortedSet of I;

theorem
  A is_transformable_to B & B is_transformable_to C
  implies A is_transformable_to C
proof
  assume
A1: A is_transformable_to B & B is_transformable_to C;
  thus thesis
  proof
    let i be set;
    assume i in I;
    then (B.i = {} implies A.i = {}) & (C.i = {} implies B.i = {})
    by A1,PZFMISC1:def 3;
    hence C.i = {} implies A.i = {};
  end;
end;

theorem Th12:
  for x be set, A be ManySortedSet of {x} holds A = x .--> A.x
proof
  let x be set;
  let A be ManySortedSet of {x};
A1: dom A = {x} by PBOOLE:def 3;
  then rng A = {A.x} by FUNCT_1:14;
  hence thesis by A1,FUNCOP_1:15;
end;

theorem Th13:
  for F, G, H be Function-yielding Function
  holds (H ** G) ** F = H ** (G ** F)
proof
  let F, G, H be Function-yielding Function;
  set f = (H ** G) ** F, g = H ** (G ** F);
  now
A1: dom f = (dom (H ** G)) /\ dom F by PBOOLE:def 24
      .= (dom H) /\ (dom G) /\ (dom F) by PBOOLE:def 24;
    then
A2: dom f = (dom H) /\ ((dom G) /\ dom F) by XBOOLE_1:16;
    hence
A3: dom f = (dom H) /\ (dom (G ** F)) by PBOOLE:def 24
      .= dom g by PBOOLE:def 24;
    let x be set;
    assume
A4: x in dom f;
    then x in (dom H) /\ (dom G) by A1,XBOOLE_0:def 3;
    then
A5: x in dom (H ** G) by PBOOLE:def 24;
    x in (dom G) /\ (dom F) by A2,A4,XBOOLE_0:def 3;
    then
A6: x in dom (G ** F) by PBOOLE:def 24;
    thus f.x = ((H**G).x) * (F.x) by A4,PBOOLE:def 24
      .= (H.x)*(G.x)*(F.x) by A5,PBOOLE:def 24
      .= (H.x)*((G.x)*(F.x)) by RELAT_1:55
      .= (H.x)*((G**F).x) by A6,PBOOLE:def 24
      .= g.x by A3,A4,PBOOLE:def 24;
  end;
  hence thesis by FUNCT_1:9;
end;

theorem Th14:
  for A, B be non-empty ManySortedSet of I
  for F be ManySortedFunction of A, B st F is "1-1" "onto"
  holds F"" is "1-1" "onto"
proof
  let A, B be non-empty ManySortedSet of I;
  let F be ManySortedFunction of A, B;
  assume
A1: F is "1-1" "onto";
  now
    let i be set;
    assume
A2: i in I;
    then reconsider g = F.i as Function of A.i, B.i by PBOOLE:def 18;
    g is one-to-one by A1,A2,MSUALG_3:1;
    then g" is one-to-one;
    hence (F"".i) is one-to-one by A1,A2,MSUALG_3:def 5;
  end;
  hence F"" is "1-1" by MSUALG_3:1;
  thus F"" is "onto"
  proof
    let i be set;
    assume
A3: i in I;
    then
A4: A.i <> {} & B.i <> {};
    reconsider g = F.i as Function of A.i, B.i by A3,PBOOLE:def 18;
A5: g is one-to-one by A1,A3,MSUALG_3:1;
    A.i = dom g by A4,FUNCT_2:def 1
      .= rng (g") by A5,FUNCT_1:55;
    hence rng (F"".i) = A.i by A1,A3,MSUALG_3:def 5;
  end;
end;

theorem
  for A, B be non-empty ManySortedSet of I
  for F be ManySortedFunction of A, B st F is "1-1" "onto" holds (F"")"" = F
proof
  let A, B be non-empty ManySortedSet of I;
  let F be ManySortedFunction of A, B;
  assume
A1: F is "1-1" "onto";
  now
    let i be set;
    assume
A2: i in I;
    then reconsider f' = (F"").i as Function of B.i, A.i by PBOOLE:def 18;
    reconsider f = F.i as Function of A.i, B.i by A2,PBOOLE:def 18;
    F"" is "1-1" "onto" by A1,Th14;
    then
A3: (F"")"".i = f'" by A2,MSUALG_3:def 5;
    f is one-to-one by A1,A2,MSUALG_3:1;
    then (f")" = f by FUNCT_1:65;
    hence (F"")"".i = F.i by A1,A2,A3,MSUALG_3:def 5;
  end;
  hence thesis by PBOOLE:3;
end;

theorem Th16:
  for F, G being Function-yielding Function st F is "1-1" & G is "1-1"
  holds G ** F is "1-1"
proof
  let F, G be Function-yielding Function such that
A1: F is "1-1" & G is "1-1";
  let i be set, f be Function such that
A2: i in dom (G**F) and
A3: (G**F).i = f;
  dom (G**F) = (dom G) /\ (dom F) by PBOOLE:def 24;
  then i in dom G & i in dom F by A2,XBOOLE_0:def 3;
  then G.i is one-to-one & F.i is one-to-one by A1,MSUALG_3:def 2;
  then (G.i)*(F.i) is one-to-one;
  hence f is one-to-one by A2,A3,PBOOLE:def 24;
end;

theorem Th17:
  for B, C be non-empty ManySortedSet of I for F be ManySortedFunction of A, B
  for G be ManySortedFunction of B, C st F is "onto" & G is "onto"
  holds G ** F is "onto"
proof
  let B, C be non-empty ManySortedSet of I;
  let F be ManySortedFunction of A, B;
  let G be ManySortedFunction of B, C;
  assume that
A1: F is "onto" and
A2: G is "onto";
  now
    let i be set;
    assume
A3: i in I;
    then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 18;
    reconsider g = G.i as Function of B.i, C.i by A3,PBOOLE:def 18;
A4: B.i <> {} by A3;
A5: C.i <> {} by A3;
    rng f = B.i & rng g = C.i by A1,A2,A3,MSUALG_3:def 3;
    then rng (g * f) = C.i by A4,A5,FUNCT_2:20;
    hence rng ((G ** F).i) = C.i by A3,MSUALG_3:2;
  end;
  hence thesis by MSUALG_3:def 3;
end;

theorem
  for A, B, C be non-empty ManySortedSet of I
  for F be ManySortedFunction of A, B for G be ManySortedFunction of B, C st
  F is "1-1" "onto" & G is "1-1" "onto" holds (G ** F)"" = (F"") ** (G"")
proof
  let A, B, C be non-empty ManySortedSet of I;
  let F be ManySortedFunction of A, B;
  let G be ManySortedFunction of B, C;
  assume that
A1: F is "1-1" "onto" and
A2: G is "1-1" "onto";
  now
    let i be set;
    assume
A3: i in I;
    then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 18;
    reconsider g = G.i as Function of B.i, C.i by A3,PBOOLE:def 18;
A4: (F"").i = f" by A1,A3,MSUALG_3:def 5;
A5: (G"").i = g" by A2,A3,MSUALG_3:def 5;
A6: (G ** F) is "1-1" "onto" by A1,A2,Th16,Th17;
A7: f is one-to-one by A1,A3,MSUALG_3:1;
A8: g is one-to-one by A2,A3,MSUALG_3:1;
    (G ** F).i = g * f by A3,MSUALG_3:2;
    then
A9: ((G ** F)"").i = (g * f)" by A3,A6,MSUALG_3:def 5;
    rng f = B.i by A1,A3,MSUALG_3:def 3;
    then reconsider ff = (F"").i as Function of B.i, A.i by A4,A7,FUNCT_2:31;
    rng g = C.i by A2,A3,MSUALG_3:def 3;
    then reconsider gg = (G"").i as Function of C.i, B.i by A5,A8,FUNCT_2:31;
    ((F"") ** (G"")).i = ff * gg by A3,MSUALG_3:2
      .= ff * (g") by A2,A3,MSUALG_3:def 5
      .= f" * g" by A1,A3,MSUALG_3:def 5;
    hence ((G ** F)"").i = ((F"") ** (G"")).i by A7,A8,A9,FUNCT_1:66;
  end;
  hence thesis by PBOOLE:3;
end;

theorem Th19:
  for A, B be non-empty ManySortedSet of I for F be ManySortedFunction of A, B
  for G be ManySortedFunction of B, A st
  F is "1-1" & F is "onto" & G ** F = id A holds G = F""
proof
  let A, B be non-empty ManySortedSet of I;
  let F be ManySortedFunction of A, B;
  let G be ManySortedFunction of B, A;
  assume
A1: F is "1-1" & F is "onto" & G ** F = id A;
  now
    let i be set;
    assume
A2: i in I;
    then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 18;
    reconsider g = G.i as Function of B.i, A.i by A2,PBOOLE:def 18;
A3: (F"").i = f" by A1,A2,MSUALG_3:def 5;
    now
      thus A.i <> {} by A2;
      thus B.i <> {} by A2;
      thus rng f = B.i by A1,A2,MSUALG_3:def 3;
      (G ** F).i = id (A.i) by A1,A2,MSUALG_3:def 1;
      hence g*f = id (A.i) by A2,MSUALG_3:2;
      thus f is one-to-one by A1,A2,MSUALG_3:1;
    end;
    hence G.i = (F"").i by A3,FUNCT_2:36;
  end;
  hence thesis by PBOOLE:3;
end;

begin

:: On the Group of Automorphisms of Many Sorted Algebra

reserve S for non void non empty ManySortedSign,
  U1, U2 for non-empty MSAlgebra over S;

canceled;

theorem Th21:
  for A, B be ManySortedSet of I st A is_transformable_to B
  for x be set st x in product MSFuncs(A, B)
  holds x is ManySortedFunction of A, B
proof
  let A, B be ManySortedSet of I;
  assume
A1: A is_transformable_to B;
  let x be set;
  assume
A2: x in product MSFuncs(A, B);
  set f = MSFuncs(A, B);
  consider g be Function such that
A3: x = g & dom g = dom f &
  for i be set st i in dom f holds g.i in f.i by A2,CARD_3:def 5;
A4: dom f = I & dom g = I by A3,PBOOLE:def 3;
A5: for i be set st i in I holds g.i in Funcs(A.i, B.i)
  proof
    let i be set;
    assume
A6: i in I;
    then MSFuncs(A, B).i = Funcs(A.i, B.i) by PBOOLE:def 22;
    hence thesis by A3,A4,A6;
  end;
A7: for i be set st i in I holds ex F be Function st F = g.i & dom F = A.i &
  rng F c= B.i
  proof
    let i be set;
    assume i in I;
    then g.i in Funcs(A.i, B.i) by A5;
    hence thesis by FUNCT_2:def 2;
  end;
A8: for i be set st i in I holds g.i is Function of A.i, B.i
  proof
    let i be set;
    assume
A9: i in I;
    then consider F be Function such that
A10: F = g.i & dom F = A.i & rng F c= B.i by A7;
    B.i = {} implies A.i = {} by A1,A9,PZFMISC1:def 3;
    hence thesis by A10,FUNCT_2:def 1,RELSET_1:11;
  end;
  g is ManySortedSet of I by A3,PBOOLE:def 3;
  hence thesis by A3,A8,PBOOLE:def 18;
end;

theorem Th22:
  for A, B be ManySortedSet of I st A is_transformable_to B
  for g be ManySortedFunction of A, B holds g in product MSFuncs(A, B)
proof
  let A, B be ManySortedSet of I;
  assume
A1: A is_transformable_to B;
  let g be ManySortedFunction of A, B;
  set f = MSFuncs(A, B);
A2: dom g = I & dom f = I by PBOOLE:def 3;
  now
    let x be set;
    assume
A3: x in dom f;
    then reconsider i = x as Element of I by PBOOLE:def 3;
A4: g.i is Function of A.i, B.i by A2,A3,PBOOLE:def 18;
    B.i = {} implies A.i = {} by A1,A2,A3,PZFMISC1:def 3;
    then g.i in Funcs(A.i, B.i) by A4,FUNCT_2:11;
    hence g.x in f.x by A2,A3,PBOOLE:def 22;
  end;
  hence thesis by A2,CARD_3:18;
end;

theorem Th23:
  for A, B be ManySortedSet of I st A is_transformable_to B
  holds MSFuncs(A, B) is non-empty
proof
  let A, B be ManySortedSet of I;
  assume
A1: A is_transformable_to B;
A2: for i be set st i in I holds Funcs(A.i, B.i) <> {}
  proof
    let i be set;
    assume i in I;
    then B.i = {} implies A.i = {} by A1,PZFMISC1:def 3;
    hence thesis by FUNCT_2:11;
  end;
  for i be set st i in I holds MSFuncs(A, B).i <> {}
  proof
    let i be set;
    assume
A3: i in I;
    then MSFuncs(A, B).i = Funcs(A.i, B.i) by PBOOLE:def 22;
    hence thesis by A2,A3;
  end;
  then for i be set st i in I holds MSFuncs(A, B).i is non empty;
  hence thesis by PBOOLE:def 16;
end;

definition
  let I, A, B;
  assume
A1: A is_transformable_to B;
  canceled 2;
  mode MSFunctionSet of A, B -> non empty set means
    :Def6:
    for x be set st x in it holds x is ManySortedFunction of A, B;
  existence
  proof
    MSFuncs(A, B) is non-empty by A1,Th23;
    then not ({} in rng MSFuncs(A, B)) by PBOOLE:149;
    then reconsider X = product MSFuncs(A, B) as non empty set by CARD_3:37;
    take X;
    let x be set;
    assume x in X;
    hence thesis by A1,Th21;
  end;
end;

registration
  let I, A;
  cluster MSFuncs(A, A) -> non-empty;
  coherence
  proof
    for i be set st i in I holds MSFuncs(A, A).i is non empty
    proof
      let i be set;
      assume
A1:   i in I;
      then (id A).i is Function of A.i, A.i by PBOOLE:def 18;
      then (id A).i in Funcs(A.i, A.i) by FUNCT_2:12;
      hence thesis by A1,PBOOLE:def 22;
    end;
    hence MSFuncs(A, A) is non-empty by PBOOLE:def 16;
  end;
end;

definition
  let S, U1, U2;
  mode MSFunctionSet of U1, U2 is MSFunctionSet of the Sorts of U1,
    the Sorts of U2;
end;

registration
  let I be set;
  let D be ManySortedSet of I;
  cluster non empty MSFunctionSet of D, D;
  existence
  proof
    not ({} in rng MSFuncs(D, D)) by PBOOLE:149;
    then reconsider X = product MSFuncs(D, D) as non empty set by CARD_3:37;
    X is MSFunctionSet of D, D
    proof
      thus D is_transformable_to D;
      let x be set;
      assume x in X;
      hence thesis by Th21;
    end;
    then reconsider X as MSFunctionSet of D, D;
    take X;
    thus thesis;
  end;
end;

definition
  let I be set;
  let D be ManySortedSet of I;
  let A be non empty MSFunctionSet of D, D;
  redefine mode Element of A -> ManySortedFunction of D, D;
  coherence by Def6;
end;

theorem
  id A is "onto"
proof
  let i be set;
  assume i in I;
  then (id A).i = id (A.i) by MSUALG_3:def 1;
  hence rng ((id A).i) = A.i by RELAT_1:71;
end;

theorem
  id A is "1-1"
proof
  now
    let i be set;
    assume i in I;
    then (id A).i = id (A.i) by MSUALG_3:def 1;
    hence (id A).i is one-to-one;
  end;
  hence thesis by MSUALG_3:1;
end;

canceled;

theorem
  id the Sorts of U1 in product MSFuncs (the Sorts of U1, the Sorts of U1)
  by Th22;

definition
  let S, U1;
  func MSAAut U1 -> MSFunctionSet of the Sorts of U1, the Sorts of U1 means
  :Def7:
  (for f be Element of it holds f is ManySortedFunction of U1, U1) &
  for h be ManySortedFunction of U1, U1 holds
  h in it iff h is_isomorphism U1, U1;
  existence
  proof
    set T = the Sorts of U1;
    defpred P[set] means ex msf be ManySortedFunction of U1, U1 st
    $1 = msf & msf is_isomorphism U1, U1;
    consider X be set such that
A1: for x be set holds x in X iff x in product MSFuncs (T, T) & P[x]
    from XBOOLE_0:sch 1;
A2: id T in product MSFuncs (T, T) by Th22;
    ex F be ManySortedFunction of U1, U1 st id T = F & F is_isomorphism U1, U1
        by MSUALG_3:16;
    then reconsider X as non empty set by A1,A2;
    X is MSFunctionSet of T, T
    proof
      thus T is_transformable_to T;
      let q be set;
      assume q in X;
      then q in product MSFuncs (T, T) &
      ex msf be ManySortedFunction of U1, U1 st
      q = msf & msf is_isomorphism U1, U1 by A1;
      hence q is ManySortedFunction of U1, U1;
    end;
    then reconsider X as MSFunctionSet of T, T;
    take X;
    thus for f be Element of X holds f is ManySortedFunction of U1, U1;
    let h be ManySortedFunction of U1, U1;
    hereby
      assume h in X;
      then h in product MSFuncs (T, T) &
      ex msf be ManySortedFunction of U1, U1 st
      h = msf & msf is_isomorphism U1, U1 by A1;
      hence h is_isomorphism U1, U1;
    end;
    assume
A3: h is_isomorphism U1, U1;
    h in product MSFuncs(T, T) by Th22;
    hence h in X by A1,A3;
  end;
  uniqueness
  proof
    set T = the Sorts of U1;
    let F1, F2 be MSFunctionSet of T, T such that
A4: ( for f be Element of F1 holds f is ManySortedFunction of U1, U1 ) &
    for h be ManySortedFunction of U1, U1 holds
    h in F1 iff h is_isomorphism U1, U1 and
A5: ( for f be Element of F2 holds f is ManySortedFunction of U1, U1 ) &
    for h be ManySortedFunction of U1, U1 holds
    h in F2 iff h is_isomorphism U1, U1;
A6: F1 c= F2
    proof
      let q be set;
      assume
A7:   q in F1;
      then reconsider h1 = q as ManySortedFunction of U1, U1 by A4;
      h1 is_isomorphism U1, U1 by A4,A7;
      hence q in F2 by A5;
    end;
    F2 c= F1
    proof
      let q be set;
      assume
A8:   q in F2;
      then reconsider h1 = q as ManySortedFunction of U1, U1 by A5;
      h1 is_isomorphism U1, U1 by A5,A8;
      hence q in F1 by A4;
    end;
    hence F1 = F2 by A6,XBOOLE_0:def 10;
  end;
end;

canceled;

theorem
  for f be Element of MSAAut U1 holds
  f in product MSFuncs (the Sorts of U1, the Sorts of U1) by Th22;

theorem
  MSAAut U1 c= product MSFuncs (the Sorts of U1, the Sorts of U1)
proof
  let q be set;
  assume q in MSAAut U1;
  then consider f be Element of MSAAut U1 such that
A1: f = q;
  thus thesis by A1,Th22;
end;

Lm3: for f be Element of MSAAut U1 holds f is "1-1" & f is "onto"
proof
  let f be Element of MSAAut U1;
  f is_isomorphism U1, U1 by Def7;
  hence thesis by MSUALG_3:13;
end;

theorem Th31:
  id the Sorts of U1 in MSAAut U1
proof
  id the Sorts of U1 is_isomorphism U1, U1 by MSUALG_3:16;
  hence thesis by Def7;
end;

theorem Th32:
  for f be Element of MSAAut U1 holds f"" in MSAAut U1
proof
  let f be Element of MSAAut U1;
  f is_isomorphism U1, U1 by Def7;
  then f"" is_isomorphism U1, U1 by MSUALG_3:14;
  hence thesis by Def7;
end;

theorem Th33:
  for f1, f2 be Element of MSAAut U1 holds f1 ** f2 in MSAAut U1
proof
  let f1, f2 be Element of MSAAut U1;
  (f1 is_isomorphism U1, U1) & (f2 is_isomorphism U1, U1) by Def7;
  then f1 ** f2 is_isomorphism U1, U1 by MSUALG_3:15;
  hence thesis by Def7;
end;

theorem Th34:
  for F be ManySortedFunction of MSAlg UA, MSAlg UA
  for f be Element of UAAut UA st F = 0 .--> f holds F in MSAAut MSAlg UA
proof
  let F be ManySortedFunction of MSAlg UA, MSAlg UA;
  let f be Element of UAAut UA;
  assume F = 0 .--> f;
  then
A1: F = MSAlg f by MSUHOM_1:def 3;
  f is_isomorphism UA, UA by Def1;
  then MSAlg f is_isomorphism MSAlg UA, MSAlg UA Over MSSign UA
  by MSUHOM_1:20;
  then F is_isomorphism MSAlg UA, MSAlg UA by A1,MSUHOM_1:9;
  hence thesis by Def7;
end;

definition
  let S, U1;
  func MSAAutComp U1 -> BinOp of MSAAut U1 means
  :Def8:
  for x, y be Element of MSAAut U1 holds it.(x, y) = y ** x;
  existence
  proof
    defpred P[Element of MSAAut U1,Element of MSAAut U1,set]
    means $3 = $2 ** $1;
A1: for x, y be Element of MSAAut U1 ex m be Element of MSAAut U1 st P[x,y,m]
    proof
      let x, y be Element of MSAAut U1;
      reconsider xx = x, yy = y as ManySortedFunction of U1, U1;
      reconsider m = yy ** xx as Element of MSAAut U1 by Th33;
      take m;
      thus thesis;
    end;
    thus ex IT being BinOp of MSAAut U1 st
    for x, y be Element of MSAAut U1 holds P[x,y,IT.(x, y)] from
    BINOP_1:sch 3(A1);
  end;
  uniqueness
  proof
    let b1, b2 be BinOp of MSAAut U1 such that
A2: for x, y be Element of MSAAut U1 holds b1.(x, y) = y ** x and
A3: for x, y be Element of MSAAut U1 holds b2.(x, y) = y ** x;
    for x, y be Element of MSAAut U1 holds b1.(x, y) = b2.(x, y)
    proof
      let x, y be Element of MSAAut U1;
      thus b1.(x, y) = y ** x by A2
        .= b2.(x, y) by A3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let S, U1;
  func MSAAutGroup U1 -> Group equals
  multMagma (# MSAAut U1, MSAAutComp U1 #);
  coherence
  proof
    set H = multMagma (# MSAAut U1, MSAAutComp U1 #);
    set SO = the Sorts of U1;
    H is associative Group-like
    proof
      thus for f, g, h be Element of H holds (f * g) * h = f * (g * h)
      proof
        let f, g, h be Element of H;
        reconsider A = f, B = g, C = h as Element of MSAAut U1;
A1:     f * g = B ** A by Def8;
A2:     g * h = C ** B by Def8;
        thus (f * g) * h = C ** (B ** A) by A1,Def8
          .= (C ** B) ** A by Th13
          .= f * (g * h) by A2,Def8;
      end; thus
      ex e be Element of H st for h be Element of H holds
      h * e = h & e * h = h & ex g be Element of H st h * g = e & g * h = e
      proof
        reconsider e = id SO as Element of H by Th31;
        take e;
        let h be Element of H;
        consider A be Element of MSAAut U1 such that
A3:     A = h;
A4:     A is "onto" & A is "1-1" by Lm3;
        h * e = (id SO) ** A by A3,Def8
          .= A by MSUALG_3:4;
        hence h * e = h by A3;
        e * h = A ** (id SO) by A3,Def8
          .= A by MSUALG_3:3;
        hence e * h = h by A3;
        reconsider g = A"" as Element of H by Th32;
        take g;
        thus h * g = (A"") ** A by A3,Def8
          .= e by A4,MSUALG_3:5;
        thus g * h = A ** (A"") by A3,Def8
          .= e by A4,MSUALG_3:5;
      end;
    end;
    hence thesis;
  end;
end;

registration
  let S, U1;
  cluster MSAAutGroup U1 -> strict;
  coherence;
end;

theorem
  for x, y be Element of MSAAutGroup U1
  for f, g be Element of MSAAut U1 st x = f & y = g holds x * y = g ** f
  by Def8;

theorem Th36:
  id the Sorts of U1 = 1_MSAAutGroup U1
proof
  set T = the Sorts of U1;
  reconsider g = id T as Element of MSAAutGroup U1 by Th31;
  consider g1 be ManySortedFunction of T, T such that
A1: g1 = g;
  consider f be Element of MSAAutGroup U1;
  f is Element of MSAAut U1;
  then consider f1 be ManySortedFunction of T, T such that
A2: f1 = f;
  g * f = f1 ** g1 by A1,A2,Def8
    .= f by A1,A2,MSUALG_3:3;
  hence thesis by GROUP_1:15;
end;

theorem
  for f be Element of MSAAut U1
  for g be Element of MSAAutGroup U1 st f = g holds f"" = g"
proof
  let f be Element of MSAAut U1;
  let g be Element of MSAAutGroup U1;
  assume
A1: f = g;
  consider g1 be Element of MSAAut U1 such that
A2: g1 = g";
A3: f is "1-1" & f is "onto" by Lm3;
  g1 ** f = g * g" by A1,A2,Def8;
  then g1 ** f = 1_MSAAutGroup U1 by GROUP_1:def 6;
  then g1 ** f = id the Sorts of U1 by Th36;
  hence thesis by A2,A3,Th19;
end;

begin

:: On the Relationship of Automorphisms of 1-Sorted and Many Sorted Algebras

theorem Th38:
  for UA1, UA2 be Universal_Algebra st UA1, UA2 are_similar
  for F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1)
  holds F.0 is Function of UA1, UA2
proof
  let UA1, UA2 be Universal_Algebra;
  assume
A1: UA1, UA2 are_similar;
  let F be ManySortedFunction of MSAlg UA1, (MSAlg UA2 Over MSSign UA1);
A2: MSSign UA1 = MSSign UA2 by A1,MSUHOM_1:10;
  reconsider f = (*-->0)*(signature UA1) as
  Function of dom signature(UA1), {0}* by MSUALG_1:7;
A3: the carrier of MSSign UA1 = {0} &
  the OperSymbols of MSSign UA1 = dom signature UA1 &
  the Arity of MSSign UA1 = f &
  the ResultSort of MSSign UA1 = dom signature UA1-->0 by MSUALG_1:def 13;
A4: 0 in {0} by TARSKI:def 1;
A5: (MSSorts UA1).0 = (0 .--> the carrier of UA1).0 by MSUALG_1:def 14
    .= the carrier of UA1 by A4,FUNCOP_1:13;
A6: MSAlg UA1 = MSAlgebra (#MSSorts UA1, MSCharact UA1#) by MSUALG_1:def 16;
A7: (MSSorts UA2).0 = (0 .--> the carrier of UA2).0 by MSUALG_1:def 14
    .= the carrier of UA2 by A4,FUNCOP_1:13;
A8: MSAlg UA2 = MSAlgebra (#MSSorts UA2, MSCharact UA2#) by MSUALG_1:def 16;
  MSAlg UA2 Over MSSign UA1 = MSAlg UA2 by A2,MSUHOM_1:9;
  hence thesis by A3,A4,A5,A6,A7,A8,PBOOLE:def 18;
end;

theorem Th39:
  for f be Element of UAAut UA
  holds 0 .--> f is ManySortedFunction of MSAlg UA, MSAlg UA
proof
  let f be Element of UAAut UA;
  MSAlg f is ManySortedFunction of MSAlg UA, MSAlg UA by MSUHOM_1:9;
  hence thesis by MSUHOM_1:def 3;
end;

Lm4: for h be Function st (dom h = UAAut UA &
for x be set st x in UAAut UA holds h.x = 0 .--> x)
holds rng h = MSAAut (MSAlg UA)
proof
  let h be Function such that
A1: dom h = UAAut UA & for x be set st x in UAAut UA holds h.x = 0 .--> x;
  thus rng h = MSAAut (MSAlg UA)
  proof
    thus rng h c= MSAAut (MSAlg UA)
    proof
      let x be set;
      assume x in rng h;
      then consider q be set such that
A2:   q in dom h & x = h.q by FUNCT_1:def 5;
A3:   x = 0 .--> q by A1,A2;
      0 .--> q is ManySortedFunction of MSAlg UA, MSAlg UA by A1,A2,Th39;
      then consider d be ManySortedFunction of MSAlg UA, MSAlg UA such that
A4:   d = x by A3;
      consider q' be Element of UAAut UA such that
A5:   q' = q by A1,A2;
      q' is_isomorphism UA, UA by Def1;
      then
A6:   MSAlg q' is_isomorphism MSAlg UA, MSAlg UA Over MSSign UA
      by MSUHOM_1:20;
      MSAlg q' = 0 .--> q by A5,MSUHOM_1:def 3
        .= x by A1,A2;
      then d is_isomorphism MSAlg UA, MSAlg UA by A4,A6,MSUHOM_1:9;
      hence thesis by A4,Def7;
    end;
    thus MSAAut (MSAlg UA) c= rng h
    proof
      let x be set;
      assume
A7:   x in MSAAut (MSAlg UA);

then reconsider f = x as ManySortedFunction of MSAlg UA, MSAlg UA by Def7;
A8:   f is_isomorphism MSAlg UA, MSAlg UA by A7,Def7;
      reconsider g = (*-->0)*(signature UA) as
      Function of dom signature UA, {0}* by MSUALG_1:7;
      the carrier of MSSign UA = {0} &
      the OperSymbols of MSSign UA = dom signature UA &
      the Arity of MSSign UA = g &
      the ResultSort of MSSign UA = dom signature UA -->0 by MSUALG_1:def 13;
      then
A9:   f = 0 .--> f.0 by Th12;
      ex q be set st q in dom h & x = h.q
      proof
        take q = f.0;
        f is ManySortedFunction of MSAlg UA, (MSAlg UA Over MSSign UA)
        by MSUHOM_1:9;
        then reconsider q' = q as Function of UA, UA by Th38;
        MSAlg q' = f by A9,MSUHOM_1:def 3;
        then MSAlg q' is_isomorphism MSAlg UA, (MSAlg UA Over MSSign UA)
        by A8,MSUHOM_1:9;
        then q' is_isomorphism UA, UA by MSUHOM_1:24;
        hence q in dom h by A1,Def1;
        hence x = h.q by A1,A9;
      end;
      hence thesis by FUNCT_1:def 5;
    end;
  end;
end;

theorem Th40:
  for h be Function st (dom h = UAAut UA &
  for x be set st x in UAAut UA holds h.x = 0 .--> x)
  holds h is Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
proof
  let h be Function such that
A1: dom h = UAAut UA & for x be set st x in UAAut UA holds h.x = 0 .--> x;
  set G = UAAutGroup UA;
  set H = MSAAutGroup (MSAlg UA);
  rng h c= the carrier of H by A1,Lm4;
  then reconsider h' = h as Function of the carrier of G, the carrier of H
  by A1,FUNCT_2:def 1,RELSET_1:11;
  now
    let a, b be Element of UAAutGroup UA;
    thus h'.(a * b) = (h'.a) * (h'.b)
    proof
      reconsider a' = a, b' = b as Element of UAAut UA;
      reconsider A = 0 .--> a', B = 0 .--> b' as
      ManySortedFunction of MSAlg UA, MSAlg UA by Th39;
      reconsider A' = A, B' = B as Element of MSAAutGroup MSAlg UA by Th34;
      reconsider ha = h'.a, hb = h'.b as Element of MSAAut MSAlg UA;
A2:   ha = A' & hb = B' by A1;
A3:   h'.(b' * a') = 0 .--> (b' * a') by A1,Th7;
      thus h'.(a * b) = h'.(b' * a') by Def2
        .= MSAlg (b' * a') by A3,MSUHOM_1:def 3
        .= (MSAlg b') ** (MSAlg a') by MSUHOM_1:26
        .= B ** MSAlg a' by MSUHOM_1:def 3
        .= B ** A by MSUHOM_1:def 3
        .= h'.a * h'.b by A2,Def8;
    end;
  end;
  hence thesis by GROUP_6:def 7;
end;

theorem Th41:
  for h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA) st
  for x be set st x in UAAut UA holds h.x = 0 .--> x holds h is bijective
proof
  let h be Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA);
  assume
A1: for x be set st x in UAAut UA holds h.x = 0 .--> x;
  set G = UAAutGroup UA;
  thus h is bijective
  proof
    thus h is one-to-one
    proof
      thus h is one-to-one
      proof
        for a, b be Element of G st h.a = h.b holds a = b
        proof
          let a, b be Element of G;
          assume
A2:       h.a = h.b;
A3:       h.a = 0 .--> a by A1
            .= [:{0}, {a}:];
          h.b = 0 .--> b by A1
            .= [:{0}, {b}:];
          then {a} = {b} by A2,A3,ZFMISC_1:134;
          hence thesis by ZFMISC_1:6;
        end;
        hence thesis by GROUP_6:1;
      end;
    end;
    thus h is onto
    proof
      dom h = UAAut UA by FUNCT_2:def 1;
      hence rng h = the carrier of MSAAutGroup (MSAlg UA) by A1,Lm4;
    end;
  end;
end;

theorem
  UAAutGroup UA, MSAAutGroup (MSAlg UA) are_isomorphic
proof
  deffunc F(set) = 0 .--> $1;
  consider h be Function such that
A1: dom h = UAAut UA
  & for x be set st x in UAAut UA holds h.x = F(x) from FUNCT_1:sch 3;
  reconsider h as Homomorphism of UAAutGroup UA, MSAAutGroup (MSAlg UA)
  by A1,Th40;
  take h;
  thus thesis by A1,Th41;
end;