The Mizar article:

Classes of Conjugation. Normal Subgroups

by
Wojciech A. Trybulec

Received August 10, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: GROUP_3
[ MML identifier index ]


environ

 vocabulary REALSET1, GROUP_2, INT_1, RELAT_1, GROUP_1, BINOP_1, VECTSP_1,
      FUNCT_1, FINSET_1, CARD_1, ABSVALUE, BOOLE, TARSKI, RLSUB_1, SETFAM_1,
      ARYTM_1, GROUP_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
      BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, RLVECT_1, FINSET_1,
      VECTSP_1, GROUP_2, DOMAIN_1, CARD_1, INT_1, GROUP_1;
 constructors WELLORD2, REAL_1, BINOP_1, GROUP_2, DOMAIN_1, NAT_1, MEMBERED,
      XBOOLE_0;
 clusters SUBSET_1, FUNCT_1, FINSET_1, GROUP_2, GROUP_1, STRUCT_0, RELSET_1,
      INT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions XBOOLE_0, BINOP_1, FUNCT_1, GROUP_2, TARSKI, VECTSP_1;
 theorems ABSVALUE, BINOP_1, CARD_1, CARD_2, ENUMSET1, FINSET_1, FUNCT_1,
      FUNCT_2, GROUP_1, GROUP_2, TARSKI, WELLORD2, ZFMISC_1, RLVECT_1, RELAT_1,
      VECTSP_1, SETFAM_1, XBOOLE_0, XBOOLE_1;
 schemes FUNCT_1, FUNCT_2, NAT_1, SUBSET_1, XBOOLE_0;

begin

reserve x,y,y1,y2 for set;
reserve G for Group;
reserve a,b,c,d,g,h for Element of G;
reserve A,B,C,D for Subset of G;
reserve H,H1,H2,H3 for Subgroup of G;
reserve n for Nat;
reserve i for Integer;

theorem Th1:
 a * b * b" = a & a * b" * b = a & b" * b * a = a & b * b" * a = a &
 a * (b * b") = a & a * (b" * b) = a & b" * (b * a) = a & b * (b" * a) = a
  proof
   thus A1: a * b * b" = a * (b * b") by VECTSP_1:def 16
                     .= a * 1.G by GROUP_1:def 5
                     .= a by GROUP_1:def 4;
   thus A2: a * b" * b = a * (b" * b) by VECTSP_1:def 16
                     .= a * 1.G by GROUP_1:def 5
                     .= a by GROUP_1:def 4;
   thus A3: b" * b * a = 1.G * a by GROUP_1:def 5
                     .= a by GROUP_1:def 4;
   thus b * b" * a = 1.G * a by GROUP_1:def 5
                  .= a by GROUP_1:def 4;
   hence thesis by A1,A2,A3,VECTSP_1:def 16;
  end;

Lm1: for A be commutative Group, a, b be Element of A
  holds a * b = b * a;

theorem
   G is commutative Group iff the mult of G is commutative
  proof
   thus G is commutative Group implies the mult of G is commutative
    proof assume A1: G is commutative Group;
     let a,b;
     thus (the mult of G).(a,b) = a * b by VECTSP_1:def 10
                                   .= b * a by A1,Lm1
                                   .= (the mult of G).(b,a) by VECTSP_1:def 10;
    end;
   assume A2: the mult of G is commutative;
     G is commutative
    proof
     let a,b;
     thus a * b = (the mult of G).(a,b) by VECTSP_1:def 10
               .= (the mult of G).(b,a) by A2,BINOP_1:def 2
               .= b * a by VECTSP_1:def 10;
    end;
   hence thesis;
  end;

theorem
   (1).G is commutative
  proof let a,b be Element of (1).G;
      a in the carrier of (1).G & b in the carrier of (1).G;
    then a in {1.G} & b in {1.G} by GROUP_2:def 7;
    then a = 1.G & b = 1.G by TARSKI:def 1;
   hence a * b = b * a;
  end;

theorem Th4:
 A c= B & C c= D implies A * C c= B * D
  proof assume A1: A c= B & C c= D;
   let x;
    assume x in A * C;
     then consider a,c such that A2: x = a * c & a in A & c in
 C by GROUP_2:12;
      thus thesis by A1,A2,GROUP_2:12;
  end;

theorem Th5:
 A c= B implies a * A c= a * B & A * a c= B * a
  proof a * A = {a} * A & a * B = {a} * B & A * a = A * {a} & B * a = B * {a}
                                                      by GROUP_2:def 3,def 4;
   hence thesis by Th4;
  end;

theorem Th6:
 H1 is Subgroup of H2 implies a * H1 c= a * H2 & H1 * a c= H2 * a
  proof assume H1 is Subgroup of H2;
    then the carrier of H1 c= the carrier of H2 &
         carr H1 = the carrier of H1 & the carrier of H2 = carr H2 &
         a * H1 = a * carr H1 & a * H2 = a * carr H2 &
         H1 * a = carr H1 * a & H2 * a = carr H2 * a
                             by GROUP_2:def 5,def 9,def 13,def 14;
   hence thesis by Th5;
  end;

theorem Th7:
 a * H = {a} * H
  proof
   thus a * H = a * carr H by GROUP_2:def 13
             .= {a} * carr H by GROUP_2:def 3
             .= {a} * H by GROUP_2:def 11;
  end;

theorem Th8:
 H * a = H * {a}
  proof
   thus H * a = carr H * a by GROUP_2:def 14
             .= carr H * {a} by GROUP_2:def 4
             .= H * {a} by GROUP_2:def 12;
  end;

theorem
   a * A * H = a * (A * H)
  proof
   thus a * A * H = {a} * A * H by GROUP_2:def 3
                 .= {a} * (A * H) by GROUP_2:116
                 .= a * (A * H) by GROUP_2:def 3;
  end;

theorem Th10:
 A * a * H = A * (a * H)
  proof
   thus A * a * H = A * {a} * H by GROUP_2:def 4
                 .= A * ({a} * H) by GROUP_2:116
                 .= A * (a * H) by Th7;
  end;

theorem
   a * H * A = a * (H * A)
  proof
   thus a * H * A = {a} * H * A by Th7
                 .= {a} * (H * A) by GROUP_2:117
                 .= a * (H * A) by GROUP_2:def 3;
  end;

theorem
   A * H * a = A * (H * a)
  proof
   thus A * H * a = A * H * {a} by GROUP_2:def 4
                 .= A * (H * {a}) by GROUP_2:117
                 .= A * (H * a) by Th8;
  end;

theorem
   H * a * A = H * (a * A)
  proof
   thus H * a * A = H * {a} * A by Th8
                 .= H * ({a} * A) by GROUP_2:118
                 .= H * (a * A) by GROUP_2:def 3;
  end;

theorem
   H * A * a = H * (A * a)
  proof
   thus H * A * a = H * A * {a} by GROUP_2:def 4
                 .= H * (A * {a}) by GROUP_2:118
                 .= H * (A * a) by GROUP_2:def 4;
  end;

theorem
   H1 * a * H2 = H1 * (a * H2)
  proof
   thus H1 * a * H2 = carr H1 * a * H2 by GROUP_2:def 14
                   .= carr H1 * (a * H2) by Th10
                   .= H1 * (a * H2) by GROUP_2:def 12;
  end;

definition let G;
 func Subgroups G -> set means
  :Def1: x in it iff x is strict Subgroup of G;
 existence
  proof
     defpred P[set] means ex H being strict Subgroup of G
             st $1 = the carrier of H;
     consider B being set such that
      A1: for x holds x in B iff x in bool the carrier of G & P[x]
             from Separation;
     defpred P[set,set] means ex H being strict Subgroup of G
                st $2 = H & $1 = the carrier of H;
      A2: for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2 by GROUP_2:68;
     consider f being Function such that
      A3: for x,y holds [x,y] in f iff x in B & P[x,y] from GraphFunc(A2);
        for x holds x in B iff ex y st [x,y] in f
       proof let x;
        thus x in B implies ex y st [x,y] in f
         proof assume A4: x in B;
           then consider H being strict Subgroup of G such that
           A5: x = the carrier of H by A1;
           reconsider y = H as set;
          take y;
          thus thesis by A3,A4,A5;
         end;
         given y such that A6: [x,y] in f;
        thus thesis by A3,A6;
       end;
      then A7: B = dom f by RELAT_1:def 4;
        for y holds y in rng f iff y is strict Subgroup of G
       proof let y;
        thus y in rng f implies y is strict Subgroup of G
         proof assume y in rng f;
           then consider x such that A8: x in dom f & y = f.x by FUNCT_1:def 5;
              [x,y] in f by A8,FUNCT_1:def 4;
            then ex H being strict Subgroup of G st y = H &
 x = the carrier of H by A3;
          hence thesis;
         end;
         assume y is strict Subgroup of G;
          then reconsider H = y as strict Subgroup of G;
          reconsider x = the carrier of H as set;
             the carrier of H c= the carrier of G by GROUP_2:def 5;
           then A9: x in dom f by A1,A7;
           then [x,y] in f by A3,A7;
           then y = f.x by A9,FUNCT_1:def 4;
        hence thesis by A9,FUNCT_1:def 5;
       end;
    hence thesis;
  end;
 uniqueness
  proof let A1,A2 be set;
    defpred P[set] means $1 is strict Subgroup of G;
    assume A10: x in A1 iff P[x];
    assume A11: x in A2 iff P[x];
   thus thesis from Extensionality(A10,A11);
  end;
end;

definition let G;
 cluster Subgroups G -> non empty;
 coherence
 proof
  consider x being strict Subgroup of G;
  x in Subgroups G by Def1;
  hence thesis;
 end;
end;

canceled 2;

theorem
   for G being strict Group holds G in Subgroups G
  proof let G be strict Group;
      G is Subgroup of G by GROUP_2:63;
   hence thesis by Def1;
  end;

theorem Th19:
 G is finite implies Subgroups G is finite
  proof defpred P[set,set] means
   ex H being strict Subgroup of G st $1 = H & $2 = the carrier of H;
    assume A1: G is finite;
      A2: for x,y1,y2 st x in Subgroups G & P[x,y1] & P[x,y2] holds y1 = y2;
      A3: for x st x in Subgroups G ex y st P[x,y]
       proof let x;
         assume x in Subgroups G;
          then reconsider F = x as strict Subgroup of G by Def1;
          reconsider y = the carrier of F as set;
        take y;
        take F;
        thus thesis;
       end;
     consider f being Function such that A4: dom f = Subgroups G and
      A5: for x st x in Subgroups G holds P[x,f.x] from FuncEx(A2,A3);
      A6: rng f c= bool the carrier of G
       proof let x;
         assume x in rng f;
          then consider y such that A7: y in dom f & f.y = x by FUNCT_1:def 5;
          consider H being strict Subgroup of G such that
          A8: y = H & x = the carrier of H by A4,A5,A7;
              the carrier of H c= the carrier of G by GROUP_2:def 5;
        hence thesis by A8;
       end;
        f is one-to-one
       proof let x,y;
         assume that A9: x in dom f and A10: y in dom f and A11: f.x = f.y;
 A12:          ex H1 being strict Subgroup of G st
 x = H1 & f.x = the carrier of H1 by A4,A5,A9;
             ex H2 being strict Subgroup of G st
 y = H2 & f.y = the carrier of H2 by A4,A5,A10;
        hence thesis by A11,A12,GROUP_2:68;
       end;
      then A13: Card Subgroups G <=`
 Card bool the carrier of G by A4,A6,CARD_1:26;
        the carrier of G is finite by A1,GROUP_1:def 13;
      then bool the carrier of G is finite by FINSET_1:24;
   hence thesis by A13,CARD_2:68;
  end;

definition let G,a,b;
 func a |^ b -> Element of G equals
  :Def2:  b" * a * b;
 correctness;
end;

theorem Th20:
 a |^ b = b" * a * b & a |^ b = b" * (a * b)
  proof
   thus a |^ b = b" * a * b by Def2;
   hence a |^ b = b" * (a * b) by VECTSP_1:def 16;
  end;

theorem Th21:
 a |^ g = b |^ g implies a = b
  proof assume A1: a |^ g = b |^ g;
      a |^ g = g" * a * g & b |^ g = g" * b * g by Th20;
    then g" * a = g" * b by A1,GROUP_1:14;
   hence thesis by GROUP_1:14;
  end;

theorem Th22:
 (1.G) |^ a = 1.G
  proof
   thus (1.G) |^ a = a" * 1.G * a by Def2
               .= a" * a by GROUP_1:def 4
               .= 1.G by GROUP_1:def 5;
  end;

theorem Th23:
 a |^ b = 1.G implies a = 1.G
  proof assume a |^ b = 1.G;
    then 1.G = b" * a * b by Def2;
    then b" = b" * a by GROUP_1:20;
   hence thesis by GROUP_1:15;
  end;

theorem Th24:
 a |^ 1.G = a
  proof
   thus a |^ 1.G = (1.G)" * (a * 1.G) by Th20
               .= (1.G)" * a by GROUP_1:def 4
               .= 1.G * a by GROUP_1:16
               .= a by GROUP_1:def 4;
  end;

theorem Th25:
 a |^ a = a
  proof
   thus a |^ a = a" * a * a by Th20
             .= 1.G * a by GROUP_1:def 5
             .= a by GROUP_1:def 4;
  end;

theorem Th26:
 a |^ a" = a & a" |^ a = a"
  proof
   thus a |^ a" = a"" * a * a" by Th20
              .= a * a * a" by GROUP_1:19
              .= a by Th1;
   thus a" |^ a = a" * a" * a by Th20
              .= a" by Th1;
  end;

theorem Th27:
 a |^ b = a iff a * b = b * a
  proof
   thus a |^ b = a implies a * b = b * a
    proof assume a |^ b = a;
      then a = b" * (a * b) by Th20;
     hence thesis by GROUP_1:21;
    end;
    assume a * b = b * a;
     then a = b" * (a * b) by GROUP_1:21;
   hence thesis by Th20;
  end;

theorem Th28:
 (a * b) |^ g = a |^ g * (b |^ g)
  proof
   thus (a * b) |^ g = g" * (a * b) * g by Def2
                   .= g" * (a * 1.G * b) * g by GROUP_1:def 4
                   .= g" * (a * (g * g") * b) * g by GROUP_1:def 5
                   .= g" * (a * g * g" * b) * g by VECTSP_1:def 16
                   .= g" * (a * g * (g" * b)) * g by VECTSP_1:def 16
                   .= g" * (a * g) * (g" * b) * g by VECTSP_1:def 16
                   .= g" * a * g * (g" * b) * g by VECTSP_1:def 16
                   .= a |^ g * (g" * b) * g by Def2
                   .= a |^ g * (g" * b * g) by VECTSP_1:def 16
                   .= a |^ g * (b |^ g) by Def2;
  end;

theorem Th29:
 a |^ g |^ h = a |^ (g * h)
  proof
   thus a |^ g |^ h = h" * (a |^ g) * h by Def2
                 .= h" * (g" * a * g) * h by Def2
                 .= h" * (g" * a) * g * h by VECTSP_1:def 16
                 .= h" * g" * a * g * h by VECTSP_1:def 16
                 .= (g * h)" * a * g * h by GROUP_1:25
                 .= (g * h)" * a * (g * h) by VECTSP_1:def 16
                 .= a |^ (g * h) by Def2;
  end;

theorem Th30:
 a |^ b |^ b" = a & a |^ b" |^ b = a
  proof
   thus a |^ b |^ b" = a |^ (b * b") by Th29
                  .= a |^ 1.G by GROUP_1:def 5
                  .= a by Th24;
   thus a |^ b" |^ b = a |^ (b" * b) by Th29
                  .= a |^ 1.G by GROUP_1:def 5
                  .= a by Th24;
  end;

canceled;

theorem Th32:
 a" |^ b = (a |^ b)"
  proof
   thus a" |^ b = b" * a" * b by Th20
              .= (a * b)" * b by GROUP_1:25
              .= (a * b)" * b"" by GROUP_1:19
              .= (b" * (a * b))" by GROUP_1:25
              .= (a |^ b)" by Th20;
  end;

Lm2: now let G,a,b;
 thus a |^ 0 |^ b = (1.G) |^ b by GROUP_1:43
               .= 1.G by Th22
               .= (a |^ b) |^ 0 by GROUP_1:43;
end;

Lm3: now let n;
  assume A1: for G,a,b holds a |^ n |^ b = (a |^ b) |^ n;
 let G,a,b;
 thus a |^ (n + 1) |^ b = (a |^ n * a) |^ b by GROUP_1:49
                     .= (a |^ n |^ b) * (a |^ b) by Th28
                     .= ((a |^ b) |^ n) * (a |^ b) by A1
                     .= (a |^ b) |^ (n + 1) by GROUP_1:49;
end;

Lm4: for n,G,a,b holds a |^ n |^ b = (a |^ b) |^ n
proof
  defpred P[Nat] means a |^ $1 |^ b = (a |^ b) |^ $1;
A1: P[0] by Lm2;
A2: for k be Nat st P[k] holds P[k+1] by Lm3;
  for k be Nat holds P[k] from Ind(A1,A2);
  hence thesis;
end;

theorem
   (a |^ n) |^ b = (a |^ b) |^ n by Lm4;

theorem
   (a |^ i) |^ b = (a |^ b) |^ i
  proof
    per cases;
     suppose i >= 0;
       then i = abs i by ABSVALUE:def 1;
      hence a |^ i |^ b =(a |^ b) |^ i by Lm4;
     suppose A1: i < 0;
      hence a |^ i |^ b = (a |^ abs i)" |^ b by GROUP_1:56
                    .= (a |^ abs (i) |^ b)" by Th32
                    .= ((a |^ b) |^ abs i)" by Lm4
                    .= (a |^ b) |^ i by A1,GROUP_1:56;
  end;

theorem Th35:
 G is commutative Group implies a |^ b = a
  proof assume A1: G is commutative Group;
   thus a |^ b = b" * a * b by Def2
             .= a * b" * b by A1,Lm1
             .= a by Th1;
  end;

theorem Th36:
 (for a,b holds a |^ b = a) implies G is commutative
  proof assume A1: for a,b holds a |^ b = a;
   let a,b;
      a |^ b = a by A1;
   hence thesis by Th27;
  end;

definition let G,A,B;
 func A |^ B -> Subset of G equals
  :Def3:  {g |^ h : g in A & h in B};
 coherence
  proof set X = {g |^ h : g in A & h in B};
      X c= the carrier of G
     proof let x;
       assume x in X;
        then ex g,h st x = g |^ h & g in A & h in B;
      hence x in the carrier of G;
     end;
   hence thesis;
  end;
end;

canceled;

theorem Th38:
 x in A |^ B iff ex g,h st x = g |^ h & g in A & h in B
  proof
   thus x in A |^ B implies ex g,h st x = g |^ h & g in A & h in B
    proof assume x in A |^ B;
       then x in {g |^ h : g in A & h in B} by Def3;
     hence thesis;
    end;
    given g,h such that A1: x = g |^ h & g in A & h in B;
       x in {a |^ b : a in A & b in B} by A1;
   hence thesis by Def3;
  end;

theorem Th39:
 A |^ B <> {} iff A <> {} & B <> {}
  proof
   thus A |^ B <> {} implies A <> {} & B <> {}
    proof assume
A1:   A |^ B <> {};
      consider x being Element of A |^ B;
         ex a,b st x = a |^ b & a in A & b in B by A1,Th38;
     hence thesis;
    end;
   assume
A2:  A <> {};
    consider x being Element of A;
   assume
A3:  B <> {};
    consider y being Element of B;
    reconsider x,y as Element of G by A2,A3,TARSKI:def 3;
       x |^ y in A |^ B by A2,A3,Th38;
   hence thesis;
  end;

theorem Th40:
 A |^ B c= B" * A * B
  proof let x;
    assume x in A |^ B;
     then consider a,b such that A1: x = a |^ b & a in A & b in B by Th38;
        b" in B" by A1,GROUP_2:5;
      then b" * a in B" * A by A1,GROUP_2:12;
      then x = b" * a * b & b" * a * b in B" * A * B by A1,Th20,GROUP_2:12;
   hence thesis;
  end;

theorem Th41:
 (A * B) |^ C c= A |^ C * (B |^ C)
  proof let x;
    assume x in (A * B) |^ C;
     then consider a,b such that A1: x = a |^ b & a in A * B & b in C by Th38;
     consider g,h such that A2: a = g * h & g in A & h in B by A1,GROUP_2:12;
        x = (g |^ b) * (h |^ b) & g |^ b in A |^ C & h |^ b in
 B |^ C by A1,A2,Th28,Th38;
   hence thesis by GROUP_2:12;
  end;

theorem Th42:
 A |^ B |^ C = A |^ (B * C)
  proof
   thus A |^ B |^ C c= A |^ (B * C)
    proof let x;
      assume x in A |^ B |^ C;
       then consider a,c such that A1: x = a |^ c & a in A |^ B & c in
 C by Th38;
       consider g,h such that A2: a = g |^ h & g in A & h in B by A1,Th38;
          x = g |^ (h * c) & h * c in B * C by A1,A2,Th29,GROUP_2:12;
     hence thesis by A2,Th38;
    end;
   let x;
    assume x in A |^ (B * C);
     then consider a,b such that A3: x = a |^ b & a in A & b in B * C by Th38;
     consider g,h such that A4: b = g * h & g in B & h in C by A3,GROUP_2:12;
        a |^ g in A |^ B by A3,A4,Th38;
      then x = a |^ g |^ h & a |^ g |^ h in A |^ B |^ C by A3,A4,Th29,Th38;
   hence thesis;
  end;

theorem
   A" |^ B = (A |^ B)"
  proof
   thus A" |^ B c= (A |^ B)"
    proof let x;
      assume x in A" |^ B;
       then consider a,b such that A1: x = a |^ b & a in A" & b in B by Th38;
       consider c such that A2: a = c" & c in A by A1,GROUP_2:5;
          x = (c |^ b)" & c |^ b in A |^ B by A1,A2,Th32,Th38;
     hence thesis by GROUP_2:5;
    end;
   let x;
    assume x in (A |^ B)";
     then consider a such that A3: x = a" & a in A |^ B by GROUP_2:5;
     consider b,c such that A4: a = b |^ c & b in A & c in B by A3,Th38;
        x = b" |^ c & b" in A" by A3,A4,Th32,GROUP_2:5;
   hence thesis by A4,Th38;
  end;

theorem Th44:
 {a} |^ {b} = {a |^ b}
  proof A1: {a} |^ {b} c= {b}" * {a} * {b} by Th40;
    A2: {b}" * {a} * {b} = {b"} * {a} * {b} by GROUP_2:6
                       .= {b" * a} * {b} by GROUP_2:22
                       .= {b" * a * b} by GROUP_2:22
                       .= {a |^ b} by Th20;
      {a} |^ {b} <> {} by Th39;
   hence thesis by A1,A2,ZFMISC_1:39;
  end;

theorem
   {a} |^ {b,c} = {a |^ b,a |^ c}
  proof
   thus {a} |^ {b,c} c= {a |^ b,a |^ c}
    proof let x;
      assume x in {a} |^ {b,c};
       then consider g,h such that A1: x = g |^ h & g in {a} & h in{b,c}
         by Th38;
          g = a & (h = b or h = c) by A1,TARSKI:def 1,def 2;
     hence thesis by A1,TARSKI:def 2;
    end;
   let x;
    assume x in {a |^ b,a |^ c};
     then (x = a |^ b or x = a |^ c) & a in {a} & b in {b,c} & c in {b,c}
                                                       by TARSKI:def 1,def 2;
   hence thesis by Th38;
  end;

theorem
   {a,b} |^ {c} = {a |^ c,b |^ c}
  proof
   thus {a,b} |^ {c} c= {a |^ c,b |^ c}
    proof let x;
      assume x in {a,b} |^ {c};
       then consider g,h such that A1: x = g |^ h & g in {a,b} & h in
{c} by Th38;
          h = c & (g = b or g = a) by A1,TARSKI:def 1,def 2;
     hence thesis by A1,TARSKI:def 2;
    end;
   let x;
    assume x in {a |^ c,b |^ c};
     then (x = a |^ c or x = b |^ c) & a in {a,b} & b in {a,b} & c in {c}
                                                   by TARSKI:def 1,def 2;
   hence thesis by Th38;
  end;

theorem
   {a,b} |^ {c,d} = {a |^ c,a |^ d,b |^ c,b |^ d}
  proof
   thus {a,b} |^ {c,d} c= {a |^ c,a |^ d,b |^ c,b |^ d}
    proof let x;
      assume x in {a,b} |^ {c,d};
       then consider g,h such that A1: x = g |^ h & g in {a,b} & h in {c,d}
                                                                     by Th38;
          (g = a or g = b) & (h = c or h = d) by A1,TARSKI:def 2;
     hence thesis by A1,ENUMSET1:19;
    end;
   let x;
    assume x in {a |^ c,a |^ d,b |^ c,b |^ d};
     then (x = a |^ c or x = a |^ d or x = b |^ c or x = b |^ d) &
          a in {a,b} & b in {a,b} & c in {c,d} & d in {c,d}
                                                by ENUMSET1:18,TARSKI:def 2;
   hence thesis by Th38;
  end;

definition let G,A,g;
 func A |^ g -> Subset of G equals
  :Def4:  A |^ {g};
 correctness;
 func g |^ A -> Subset of G equals
  :Def5:  {g} |^ A;
 correctness;
end;

canceled 2;

theorem Th50:
 x in A |^ g iff ex h st x = h |^ g & h in A
  proof
   thus x in A |^ g implies ex h st x = h |^ g & h in A
    proof assume x in A |^ g;
       then x in A |^ {g} by Def4;
      then consider a,b such that A1: x = a |^ b & a in A & b in {g} by Th38;
         b = g by A1,TARSKI:def 1;
     hence thesis by A1;
    end;
    given h such that A2: x = h |^ g & h in A;
       g in {g} by TARSKI:def 1;
     then x in A |^ {g} by A2,Th38;
   hence thesis by Def4;
  end;

theorem Th51:
 x in g |^ A iff ex h st x = g |^ h & h in A
  proof
   thus x in g |^ A implies ex h st x = g |^ h & h in A
    proof assume x in g |^ A;
       then x in {g} |^ A by Def5;
      then consider a,b such that A1: x = a |^ b & a in {g} & b in A by Th38;
         a = g by A1,TARSKI:def 1;
     hence thesis by A1;
    end;
    given h such that A2: x = g |^ h & h in A;
       g in {g} by TARSKI:def 1;
     then x in {g} |^ A by A2,Th38;
   hence thesis by Def5;
  end;

theorem
   g |^ A c= A" * g * A
  proof let x;
    assume x in g |^ A;
     then consider a such that A1: x = g |^ a & a in A by Th51;
        a" in A" by A1,GROUP_2:5;
      then a" * g in A" * g by GROUP_2:34;
      then a" * g * a in A" * g * A by A1,GROUP_2:12;
   hence thesis by A1,Th20;
  end;

theorem Th53:
 A |^ B |^ g = A |^ (B * g)
  proof
   thus A |^ B |^ g = A |^ B |^ {g} by Def4
                 .= A |^ (B * {g}) by Th42
                 .= A |^ (B * g) by GROUP_2:def 4;
  end;

theorem Th54:
 A |^ g |^ B = A |^ (g * B)
  proof
   thus A |^ g |^ B = A |^ {g} |^ B by Def4
                 .= A |^ ({g} * B) by Th42
                 .= A |^ (g * B) by GROUP_2:def 3;
  end;

theorem
   g |^ A |^ B = g |^ (A * B)
  proof
   thus g |^ A |^ B = {g} |^ A |^ B by Def5
                 .= {g} |^ (A * B) by Th42
                 .= g |^ (A * B) by Def5;
  end;

theorem Th56:
 A |^ a |^ b = A |^ (a * b)
  proof
   thus A |^ a |^ b = A |^ a |^ {b} by Def4
                 .= A |^ (a * {b}) by Th54
                 .= A |^ ({a} * {b}) by GROUP_2:def 3
                 .= A |^ {a * b} by GROUP_2:22
                 .= A |^ (a * b) by Def4;
  end;

theorem
   a |^ A |^ b = a |^ (A * b)
  proof
   thus a |^ A |^ b = {a} |^ A |^ b by Def5
                 .= {a} |^ (A * b) by Th53
                 .= a |^ (A * b) by Def5;
  end;

theorem
   a |^ b |^ A = a |^ (b * A)
  proof
   thus a |^ b |^ A = {a |^ b} |^ A by Def5
                 .= {a} |^ {b} |^ A by Th44
                 .= {a} |^ ({b} * A) by Th42
                 .= a |^ ({b} * A) by Def5
                 .= a |^ (b * A) by GROUP_2:def 3;
  end;

theorem Th59:
 A |^ g = g" * A * g
  proof
      A |^ g = A |^ {g} by Def4;
    then A |^ g c= {g}" * A * {g} by Th40;
    then A |^ g c= {g"} * A * {g} by GROUP_2:6;
    then A |^ g c= {g"} * A * g by GROUP_2:def 4;
   hence A |^ g c= g" * A * g by GROUP_2:def 3;
   let x;
    assume x in g" * A * g;
     then consider a such that A1: x = a * g & a in g" * A by GROUP_2:34;
     consider b such that A2: a = g" * b & b in A by A1,GROUP_2:33;
        x = b |^ g by A1,A2,Th20;
   hence thesis by A2,Th50;
  end;

theorem
   (A * B) |^ a c= (A |^ a) * (B |^ a)
  proof
    A1: (A * B) |^ a = (A * B) |^ {a} by Def4;
      A |^ a = A |^ {a} & B |^ a = B |^ {a} by Def4;
   hence thesis by A1,Th41;
  end;

theorem Th61:
 A |^ 1.G = A
  proof
   thus A |^ 1.G = (1.G)" * A * 1.G by Th59
               .= (1.G)" * A by GROUP_2:43
               .= 1.G * A by GROUP_1:16
               .= A by GROUP_2:43;
  end;

theorem
   A <> {} implies (1.G) |^ A = {1.G}
  proof assume A1: A <> {};
   thus (1.G) |^ A c= {1.G}
    proof let x;
      assume x in (1.G) |^ A;
       then ex a st x = (1.G) |^ a & a in A by Th51;
        then x = 1.G by Th22;
     hence thesis by TARSKI:def 1;
    end;
   let x;
    assume x in {1.G};
      then A2: x = 1.G by TARSKI:def 1;
     consider y being Element of A;
     reconsider y as Element of G by A1,TARSKI:def 3;
        (1.G) |^ y = x by A2,Th22;
   hence thesis by A1,Th51;
  end;

theorem Th63:
 A |^ a |^ a" = A & A |^ a" |^ a = A
  proof
   thus A |^ a |^ a" = A |^ (a * a") by Th56
                  .= A |^ 1.G by GROUP_1:def 5
                  .= A by Th61;
   thus A |^ a" |^ a = A |^ (a" * a) by Th56
                  .= A |^ 1.G by GROUP_1:def 5
                  .= A by Th61;
  end;

canceled;

theorem Th65:
 G is commutative Group iff for A,B st B <> {} holds A |^ B = A
  proof
   thus G is commutative Group implies for A,B st B <> {} holds A |^ B = A
    proof assume A1: G is commutative Group;
     let A,B;
      assume A2: B <> {};
     thus A |^ B c= A
      proof let x;
        assume x in A |^ B;
         then ex a,b st x = a |^ b & a in A & b in B by Th38;
       hence thesis by A1,Th35;
      end;
     let x;
      assume A3: x in A;
       then reconsider a = x as Element of G;
       consider y being Element of B;
       reconsider y as Element of G by A2,TARSKI:def 3;
          a |^ y = x by A1,Th35;
     hence thesis by A2,A3,Th38;
    end;
    assume A4: for A,B st B <> {} holds A |^ B = A;
       now let a,b;
         {a} = {a} |^ {b} by A4
               .= {a |^ b} by Th44;
      hence a = a |^ b by ZFMISC_1:6;
     end;
   hence thesis by Th36;
  end;

theorem
   G is commutative Group iff for A,g holds A |^ g = A
  proof
   thus G is commutative Group implies for A,g holds A |^ g = A
    proof assume A1: G is commutative Group;
     let A,g;
        A |^ {g} = A by A1,Th65;
     hence thesis by Def4;
    end;
    assume A2: for A,g holds A |^ g = A;
       now let a,b;
         {a} = {a} |^ b by A2
          .= {a} |^ {b} by Def4
          .= {a |^ b} by Th44;
      hence a = a |^ b by ZFMISC_1:6;
     end;
   hence thesis by Th36;
  end;

theorem
   G is commutative Group iff for A,g st A <> {} holds g |^ A = {g}
  proof
   thus G is commutative Group implies for A,g st A <> {} holds g |^ A = {g}
    proof assume A1: G is commutative Group;
     let A,g;
      assume A <> {};
       then {g} |^ A = {g} by A1,Th65;
     hence thesis by Def5;
    end;
    assume A2: for A,g st A <> {} holds g |^ A = {g};
       now let a,b;
         {a} = a |^ {b} by A2
               .= {a} |^ {b} by Def5
               .= {a |^ b} by Th44;
      hence a = a |^ b by ZFMISC_1:6;
     end;
   hence thesis by Th36;
  end;

definition let G,H,a;
 func H |^ a -> strict Subgroup of G means
  :Def6: the carrier of it = carr(H) |^ a;
 existence
  proof consider H1 being strict Subgroup of G such that
     A1: the carrier of H1 = a" * H * a"" by GROUP_2:150;
      the carrier of H1 = a" * H * a by A1,GROUP_1:19
                     .= a" * carr H * a by GROUP_2:def 13
                     .= carr(H) |^ a by Th59;
   hence thesis;
  end;
 correctness by GROUP_2:68;
end;

canceled 2;

theorem Th70:
 x in H |^ a iff ex g st x = g |^ a & g in H
  proof
   thus x in H |^ a implies ex g st x = g |^ a & g in H
    proof assume x in H |^ a;
       then x in the carrier of H |^ a by RLVECT_1:def 1;
       then x in carr H |^ a by Def6;
      then consider b such that A1: x = b |^ a and A2: b in carr H by Th50;
     take b;
     thus thesis by A1,A2,GROUP_2:88;
    end;
    given g such that A3: x = g |^ a & g in H;
       g in carr H by A3,GROUP_2:88;
     then x in carr H |^ a by A3,Th50;
     then x in the carrier of H |^ a by Def6;
   hence thesis by RLVECT_1:def 1;
  end;

theorem Th71:
 the carrier of H |^ a = a" * H * a
  proof
   thus the carrier of H |^ a = carr(H) |^ a by Def6
                            .= a" * carr H * a by Th59
                            .= a" * H * a by GROUP_2:def 13;
  end;

theorem Th72:
 H |^ a |^ b = H |^ (a * b)
  proof A1: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9;
      the carrier of H |^ a |^ b = carr(H |^ a) |^ b by Def6
                            .= (carr H |^ a) |^ b by A1,Def6
                            .= carr H |^ (a * b) by Th56
                            .= the carrier of H |^ (a * b) by Def6;
   hence thesis by GROUP_2:68;
  end;

theorem Th73:
 for H being strict Subgroup of G holds H |^ 1.G = H
  proof let H be strict Subgroup of G;
      the carrier of H |^ 1.G = carr H |^ 1.G by Def6
                          .= carr H by Th61
                          .= the carrier of H by GROUP_2:def 9;
   hence thesis by GROUP_2:68;
  end;

theorem Th74:
 for H being strict Subgroup of G holds
 H |^ a |^ a" = H & H |^ a" |^ a = H
  proof let H be strict Subgroup of G;
   thus H |^ a |^ a" = H |^ (a * a") by Th72
                  .= H |^ 1.G by GROUP_1:def 5
                  .= H by Th73;
   thus H |^ a" |^ a = H |^ (a" * a) by Th72
                  .= H |^ 1.G by GROUP_1:def 5
                  .= H by Th73;
  end;

canceled;

theorem Th76:
 (H1 /\ H2) |^ a = (H1 |^ a) /\ (H2 |^ a)
  proof let g;
   thus g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a)
    proof assume g in (H1 /\ H2) |^ a;
      then consider h such that A1: g = h |^ a & h in H1 /\ H2 by Th70;
         h in H1 & h in H2 by A1,GROUP_2:99;
       then g in H1 |^ a & g in H2 |^ a by A1,Th70;
     hence thesis by GROUP_2:99;
    end;
    assume A2: g in (H1 |^ a) /\ (H2 |^ a);
       then g in H1 |^ a by GROUP_2:99;
     then consider b such that A3: g = b |^ a & b in H1 by Th70;
        g in H2 |^ a by A2,GROUP_2:99;
     then consider c such that A4: g = c |^ a & c in H2 by Th70;
        b = c by A3,A4,Th21;
      then b in (H1 /\ H2) by A3,A4,GROUP_2:99;
   hence thesis by A3,Th70;
  end;

theorem Th77:
 Ord H = Ord(H |^ a)
  proof
    deffunc F(Element of G) = $1 |^ a;
    consider f being Function of the carrier of G, the carrier of G
    such that A1: for g holds f.g = F(g) from LambdaD;
    set g = f | (the carrier of H);
A2:     dom f = the carrier of G & the carrier of H c= the carrier of G
                                      by FUNCT_2:def 1,GROUP_2:def 5;
     then A3: dom g = the carrier of H by RELAT_1:91;
     A4: rng g = the carrier of H |^ a
      proof A5: the carrier of H = carr H by GROUP_2:def 9;
       thus rng g c= the carrier of H |^ a
        proof let x;
          assume x in rng g;
           then consider y such that A6: y in dom g and A7: g.y = x
                                                             by FUNCT_1:def 5;
           reconsider y as Element of H by A2,A6,RELAT_1:91;
           reconsider y as Element of G by GROUP_2:51;
              f.y = y |^ a & f.y = g.y by A1,A6,FUNCT_1:70;
            then x in carr H |^ a by A5,A7,Th50;
         hence thesis by Def6;
        end;
       let x;
        assume x in the carrier of H |^ a;
          then x in carr H |^ a by Def6;
         then consider b such that A8: x = b |^ a and A9: b in carr H
            by Th50;
            g.b = f.b & f.b = b |^ a by A1,A3,A5,A9,FUNCT_1:70;
       hence thesis by A3,A5,A8,A9,FUNCT_1:def 5;
      end;
       g is one-to-one
      proof let x,y;
        assume that A10: x in dom g & y in dom g and A11: g.x = g.y;
         reconsider b = x, c = y as Element of H
            by A2,A10,RELAT_1:91;
         reconsider b,c as Element of G by GROUP_2:51;
            f.x = g.x & f.y = g.y & f.x = b |^ a & f.y = c |^ a
             by A1,A10,FUNCT_1:70;
       hence thesis by A11,Th21;
      end;
     then the carrier of H,the carrier of H |^ a are_equipotent
     by A3,A4,WELLORD2:def 4;
     then Card the carrier of H = Card the carrier of H |^ a by CARD_1:21;
     then Card the carrier of H = Ord(H |^ a) by GROUP_1:def 12;
   hence thesis by GROUP_1:def 12;
  end;

theorem Th78:
 H is finite iff H |^ a is finite
  proof Ord H = Card the carrier of H & Ord H = Ord(H |^ a) &
        Ord(H |^ a) = Card the carrier of H |^ a by Th77,GROUP_1:def 12;
    then the carrier of H,the carrier of H |^ a are_equipotent by CARD_1:21;
    then the carrier of H is finite iff the carrier of H |^ a is finite
                                                              by CARD_1:68;
   hence thesis by GROUP_1:def 13;
  end;

theorem Th79:
 H is finite implies ord H = ord(H |^ a)
  proof assume A1: H is finite;
     then H |^ a is finite by Th78;
     then consider C being finite set such that
A2:   C = the carrier of H |^ a & ord(H |^ a) = card C by GROUP_1:def 14;
     consider B being finite set such that
A3:   B = the carrier of H & ord H = card B by A1,GROUP_1:def 14;
       Ord H = Card the carrier of H & Ord H = Ord(H |^ a) &
     Ord(H |^ a) = Card the carrier of H |^ a by Th77,GROUP_1:def 12;
   hence thesis by A2,A3;
  end;

theorem Th80:
 (1).G |^ a = (1).G
  proof A1: the carrier of (1).G = {1.G} & carr (1).G = the carrier of (1).G
                                                      by GROUP_2:def 7,def 9;
      the carrier of (1).G |^ a = (carr (1).G) |^ a by Def6
                            .= {1.G} |^ {a} by A1,Def4
                            .= {(1.G) |^ a} by Th44
                            .= {1.G} by Th22;
   hence thesis by GROUP_2:def 7;
  end;

theorem
   for H being strict Subgroup of G holds H |^ a = (1).G implies H = (1).G
  proof let H be strict Subgroup of G;
   assume A1: H |^ a = (1).G;
    A2: (1).G is finite & ord (1).G = 1 by GROUP_2:80,81;
    then A3: H is finite by A1,Th78;
    then ord H = 1 by A1,A2,Th79;
   hence thesis by A3,GROUP_2:82;
  end;

theorem Th82:
 for G being Group, a being Element of G
  holds (Omega).G |^ a = (Omega).G
  proof let G be Group, a be Element of G;
A1: (Omega).G = the HGrStr of G by GROUP_2:def 8;
    let h be Element of G;
      A2: (h |^ a") |^ a = h |^ (a" * a) by Th29
                     .= h |^ 1.G by GROUP_1:def 5
                     .= h by Th24;
        h |^ a" in the HGrStr of G by RLVECT_1:def 1;
     hence h in (Omega).G |^ a iff h in (Omega).G by A1,A2,Th70,RLVECT_1:def 1
;
  end;

theorem
   for H being strict Subgroup of G holds
 H |^ a = G implies H = G
  proof let H be strict Subgroup of G;
   assume A1: H |^ a = G;
      now let g;
      assume A2: not g in H;
         now assume g |^ a in H |^ a;
         then ex h st g |^ a = h |^ a & h in H by Th70;
        hence contradiction by A2,Th21;
       end;
     hence contradiction by A1,RLVECT_1:def 1;
    end;
   hence thesis by A1,GROUP_2:71;
  end;

theorem Th84:
 Index H = Index(H |^ a)
  proof defpred P[set,set] means ex b st $1 = b * H & $2 = (b |^ a) * (H |^ a);
     A1: for x,y1,y2 st x in Left_Cosets H & P[x,y1] & P[x,y2] holds y1 = y2
      proof let x,y1,y2; set A = carr H;
        assume x in Left_Cosets H;
        given b such that A2: x = b * H & y1 = (b |^ a) * (H |^ a);
        given c such that A3: x = c * H & y2 = (c |^ a) * (H |^ a);
         A4: the carrier of H |^ a = carr(H |^ a) by GROUP_2:def 9;
       thus y1 = (a" * b * a) * (H |^ a) by A2,Th20
              .= (a" * b * a) * carr(H |^ a) by GROUP_2:def 13
              .= (a" * b * a) * (a" * H * a) by A4,Th71
              .= (a" * b * a) * (a" * A * a) by GROUP_2:def 13
              .= (a" * b * a) * (a" * A) * a by GROUP_2:39
              .= (a" * b) * (a * (a" * A)) * a by GROUP_2:38
              .= a" * b * (a * a" * A) * a by GROUP_2:38
              .= a" * b * (1.G * A) * a by GROUP_1:def 5
              .= a" * b * A * a by GROUP_2:43
              .= a" * (b * A) * a by GROUP_2:38
              .= a" * (c * H) * a by A2,A3,GROUP_2:def 13
              .= a" * (c * A) * a by GROUP_2:def 13
              .= a" * c * A * a by GROUP_2:38
              .= a" * c * (1.G * A) * a by GROUP_2:43
              .= a" * c * (a * a" * A) * a by GROUP_1:def 5
              .= (a" * c) * (a * (a" * A)) * a by GROUP_2:38
              .= (a" * c * a) * (a" * A) * a by GROUP_2:38
              .= (a" * c * a) * (a" * A * a) by GROUP_2:39
              .= (a" * c * a) * (a" * H * a) by GROUP_2:def 13
              .= (a" * c * a) * carr(H |^ a) by A4,Th71
              .= (a" * c * a) * (H |^ a) by GROUP_2:def 13
              .= y2 by A3,Th20;
      end;
     A5: for x st x in Left_Cosets H ex y st P[x,y]
      proof let x;
        assume x in Left_Cosets H;
         then consider b such that A6: x = b * H by GROUP_2:def 15;
         reconsider y = (b |^ a) * (H |^ a) as set;
       take y;
       take b;
       thus thesis by A6;
      end;
    consider f being Function such that A7: dom f = Left_Cosets H and
     A8: for x st x in Left_Cosets H holds P[x,f.x] from FuncEx(A1,A5);
     A9: rng f = Left_Cosets(H |^ a)
      proof
       thus rng f c= Left_Cosets(H |^ a)
        proof let x;
          assume x in rng f;
           then consider y such that A10: y in dom f & f.y = x by FUNCT_1:def 5
;
              ex b st y = b * H & x = (b |^ a) * (H |^ a)
             by A7,A8,A10;
         hence thesis by GROUP_2:def 15;
        end;
       let x;
        assume x in Left_Cosets(H |^ a);
         then consider b such that A11: x = b * (H |^ a) by GROUP_2:def 15;
         set c = b |^ a";
          A12: x = (c |^ a) * (H |^ a) by A11,Th30;
          A13: c * H in Left_Cosets H by GROUP_2:def 15;
         then consider d such that
          A14: c * H = d * H & f.(c * H) = (d |^ a) * (H |^ a) by A8;
            (c |^ a) * (H |^ a) = (d |^ a) * (H |^ a) by A1,A13,A14;
       hence thesis by A7,A12,A13,A14,FUNCT_1:def 5;
      end;
       f is one-to-one
      proof let x,y;
        assume that A15: x in dom f and A16: y in dom f and A17: f.x = f.y;
         consider b such that A18: x = b * H and A19: f.x = (b |^ a) * (H |^ a)
                                                                     by A7,A8,
A15;
         consider c such that A20: y = c * H and A21: f.y = (c |^ a) * (H |^ a)
                                                                     by A7,A8,
A16;
          A22: (c |^ a)" * (b |^ a) in H |^ a by A17,A19,A21,GROUP_2:137;
            (c |^ a)" * (b |^ a) = (c" |^ a) * (b |^ a) by Th32
                            .= (c" * b) |^ a by Th28;
         then consider d such that A23: (c" * b) |^ a = d |^ a & d in H
                                                              by A22,Th70;
            c" * b = d by A23,Th21;
       hence thesis by A18,A20,A23,GROUP_2:137;
      end;
     then A24: Left_Cosets H,Left_Cosets(H |^ a) are_equipotent
     by A7,A9,WELLORD2:def 4;
   thus Index H = Card Left_Cosets H by GROUP_2:175
               .= Card Left_Cosets(H |^ a) by A24,CARD_1:21
               .= Index(H |^ a) by GROUP_2:175;
  end;

theorem
   Left_Cosets H is finite implies index H = index(H |^ a)
  proof assume Left_Cosets H is finite;
   then consider B being finite set such that
A1:    B = Left_Cosets H & index H = card B by GROUP_2:def 18;
A2:    Index H = Card Left_Cosets H & Index(H |^ a) = Card Left_Cosets(H|^ a) &
     Index H = Index(H |^ a) by Th84,GROUP_2:175;
    then Left_Cosets H,Left_Cosets(H |^ a) are_equipotent by CARD_1:21;
      then Left_Cosets(H |^ a) is finite by A1,CARD_1:68;
   then consider C being finite set such that
A3:    C = Left_Cosets(H |^ a) & index(H |^ a) = card C by GROUP_2:def 18;
   thus thesis by A1,A2,A3;
  end;

theorem Th86:
 G is commutative Group implies
  for H being strict Subgroup of G for a holds H |^ a = H
  proof
   assume A1: G is commutative Group;
   let H be strict Subgroup of G;
   let a;
      the carrier of H |^ a = a" * H * a by Th71
                        .= H * a" * a by A1,GROUP_2:135
                        .= H * (a" * a) by GROUP_2:129
                        .= H * 1.G by GROUP_1:def 5
                        .= carr H by GROUP_2:132
                        .= the carrier of H by GROUP_2:def 9;
   hence thesis by GROUP_2:68;
  end;

definition let G,a,b;
 pred a,b are_conjugated means
  :Def7: ex g st a = b |^ g;
 antonym a,b are_not_conjugated;
end;

canceled;

theorem Th88:
 a,b are_conjugated iff ex g st b = a |^ g
  proof
   thus a,b are_conjugated implies ex g st b = a |^ g
    proof given g such that A1: a = b |^ g;
        a |^ g" = b by A1,Th30;
     hence thesis;
    end;
    given g such that A2: b = a |^ g;
       a = b |^ g" by A2,Th30;
   hence thesis by Def7;
  end;

theorem Th89:
 a,a are_conjugated
  proof take 1.G;
   thus thesis by Th24;
  end;

theorem Th90:
 a,b are_conjugated implies b,a are_conjugated
  proof given g such that A1: a = b |^ g;
      b = a |^ g" by A1,Th30;
   hence thesis by Def7;
  end;

definition let G,a,b;
 redefine pred a,b are_conjugated;
 reflexivity by Th89;
 symmetry by Th90;
end;

theorem Th91:
 a,b are_conjugated & b,c are_conjugated implies a,c are_conjugated
  proof given g such that A1: a = b |^ g;
    given h such that A2: b = c |^ h;
       a = c |^ (h * g) by A1,A2,Th29;
   hence thesis by Def7;
  end;

theorem Th92:
 a,1.G are_conjugated or 1.G,a are_conjugated implies a = 1.G
  proof assume A1: a,1.G are_conjugated or 1.G,a are_conjugated;
      now per cases by A1;
     suppose a,1.G are_conjugated;
       then ex g st 1.G = a |^ g by Th88;
      hence thesis by Th23;
     suppose 1.G,a are_conjugated;
       then ex g st 1.G = a |^ g by Def7;
      hence thesis by Th23;
    end;
   hence thesis;
  end;

theorem Th93:
 a |^ carr (Omega).G = {b : a,b are_conjugated}
  proof set A = a |^ carr (Omega).G; set B = {b : a,b are_conjugated};
   thus A c= B
    proof let x;
      assume A1: x in A;
       then A2: ex g st x = a |^ g & g in carr(Omega).G by Th51;
       reconsider b = x as Element of G by A1;
          b,a are_conjugated by A2,Def7;
     hence thesis;
    end;
   let x;
    assume x in B;
     then consider b such that A3: x = b & a,b are_conjugated;
        b,a are_conjugated by A3;
     then consider g such that A4: b = a |^ g by Def7;
        g in the HGrStr of G by RLVECT_1:def 1;
      then g in (Omega).G by GROUP_2:def 8;
      then g in carr (Omega).G by GROUP_2:88;
   hence thesis by A3,A4,Th51;
  end;

definition let G,a;
 func con_class a -> Subset of G equals
  :Def8:  a |^ carr (Omega).G;
 correctness;
end;

canceled;

theorem Th95:
 x in con_class a iff ex b st b = x & a,b are_conjugated
  proof
   thus x in con_class a implies ex b st b = x & a,b are_conjugated
    proof assume x in con_class a;
       then x in a |^ carr (Omega).G by Def8;
       then x in {b : a,b are_conjugated} by Th93;
     hence thesis;
    end;
    given b such that A1: b = x & a,b are_conjugated;
       x in {c : a,c are_conjugated} by A1;
     then x in a |^ carr (Omega).G by Th93;
   hence thesis by Def8;
  end;

theorem Th96:
 a in con_class b iff a,b are_conjugated
  proof
   thus a in con_class b implies a,b are_conjugated
    proof assume a in con_class b;
      then ex c st a = c & b,c are_conjugated by Th95;
     hence thesis;
    end;
    assume a,b are_conjugated;
   hence thesis by Th95;
  end;

theorem Th97:
 a |^ g in con_class a
  proof a,a |^ g are_conjugated by Th88;
   hence thesis by Th95;
  end;

theorem
  a in con_class a by Th96;

theorem
   a in con_class b implies b in con_class a
  proof assume a in con_class b;
    then a,b are_conjugated by Th96;
   hence thesis by Th96;
  end;

theorem
   con_class a = con_class b iff con_class a meets con_class b
  proof
   thus con_class a = con_class b implies con_class a meets con_class b
    proof assume con_class a = con_class b;
      then a in con_class b & a in con_class a by Th96;
     hence thesis by XBOOLE_0:3;
    end;
    assume con_class a meets con_class b;
     then consider x such that A1: x in con_class a & x in
 con_class b by XBOOLE_0:3;
     reconsider x as Element of G by A1;
   thus con_class a c= con_class b
    proof let y;
      assume y in con_class a;
       then consider g such that A2: g = y & a,g are_conjugated by Th95;
          x,a are_conjugated & x,b are_conjugated by A1,Th96;
        then x,g are_conjugated & b,x are_conjugated by A2,Th91;
        then b,g are_conjugated by Th91;
     hence thesis by A2,Th95;
    end;
   let y;
    assume y in con_class b;
     then consider g such that A3: g = y & b,g are_conjugated by Th95;
        x,b are_conjugated & x,a are_conjugated by A1,Th96;
      then a,x are_conjugated & x,g are_conjugated by A3,Th91;
      then a,g are_conjugated by Th91;
   hence thesis by A3,Th95;
  end;

theorem
   con_class a = {1.G} iff a = 1.G
  proof
   thus con_class a = {1.G} implies a = 1.G
    proof assume A1: con_class a = {1.G};
        a in con_class a by Th96;
     hence thesis by A1,TARSKI:def 1;
    end;
    assume A2: a = 1.G;
   thus con_class a c= {1.G}
    proof let x;
      assume x in con_class a;
       then consider b such that A3: b = x & a,b are_conjugated by Th95;
          b = 1.G by A2,A3,Th92;
     hence thesis by A3,TARSKI:def 1;
    end;
      1.G in con_class a by A2,Th96;
   hence thesis by ZFMISC_1:37;
  end;

theorem
   con_class a * A = A * con_class a
  proof
   thus con_class a * A c= A * con_class a
    proof let x;
      assume x in con_class a * A;
       then consider b,c such that A1: x = b * c & b in con_class a & c in A
                                                              by GROUP_2:12;
          b,a are_conjugated by A1,Th96;
       then consider g such that A2: b = a |^ g by Def7;
       reconsider h = x as Element of G by A1;
          h |^ c" = c"" * ((a |^ g) * c) * c" by A1,A2,Th20
              .= c * ((a |^ g) * c) * c" by GROUP_1:19
              .= c * (((a |^ g) * c) * c") by VECTSP_1:def 16
              .= c * (a |^ g) by Th1;
        then A3: x = (c * (a |^ g)) |^ c by Th30
                 .= (c |^ c) * (a |^ g |^ c) by Th28
                 .= c * (a |^ g |^ c) by Th25
                 .= c * (a |^ (g * c)) by Th29;
          a |^ (g * c) in con_class a by Th97;
     hence thesis by A1,A3,GROUP_2:12;
    end;
   let x;
    assume x in A * con_class a;
     then consider b,c such that A4: x = b * c & b in A & c in con_class a
                                                               by GROUP_2:12;
        c,a are_conjugated by A4,Th96;
     then consider g such that A5: c = a |^ g by Def7;
     reconsider h = x as Element of G by A4;
        h |^ b = b" * (b * (a |^ g)) * b by A4,A5,Th20
           .= (a |^ g) * b by Th1;
      then A6: x = ((a |^ g) * b) |^ b" by Th30
               .= (a |^ g) |^ b" * (b |^ b") by Th28
               .= a |^ (g * b") * (b |^ b") by Th29
               .= a |^ (g * b") * b by Th26;
        a |^ (g * b") in con_class a by Th97;
   hence thesis by A4,A6,GROUP_2:12;
  end;

definition let G,A,B;
 pred A,B are_conjugated means
  :Def9: ex g st A = B |^ g;
 antonym A,B are_not_conjugated;
end;

canceled;

theorem Th104:
 A,B are_conjugated iff ex g st B = A |^ g
  proof
   thus A,B are_conjugated implies ex g st B = A |^ g
    proof given g such that A1: A = B |^ g;
        A |^ g" = B by A1,Th63;
     hence thesis;
    end;
    given g such that A2: B = A |^ g;
       A = B |^ g" by A2,Th63;
   hence thesis by Def9;
  end;

theorem Th105:
 A,A are_conjugated
  proof take 1.G;
   thus thesis by Th61;
    end;

theorem Th106:
 A,B are_conjugated implies B,A are_conjugated
  proof given g such that A1: A = B |^ g;
      B = A |^ g" by A1,Th63;
   hence thesis by Def9;
  end;

definition let G,A,B;
 redefine pred A,B are_conjugated;
 reflexivity by Th105;
 symmetry by Th106;
end;

theorem Th107:
 A,B are_conjugated & B,C are_conjugated implies A,C are_conjugated
  proof given g such that A1: A = B |^ g;
    given h such that A2: B = C |^ h;
       A = C |^ (h * g) by A1,A2,Th56;
   hence thesis by Def9;
  end;

theorem Th108:
 {a},{b} are_conjugated iff a,b are_conjugated
  proof
   thus {a},{b} are_conjugated implies a,b are_conjugated
    proof assume {a},{b} are_conjugated;
      then consider g such that A1: {a} |^ g = {b} by Th104;
         {b} = {a} |^ {g} by A1,Def4
          .= {a |^ g} by Th44;
       then b = a |^ g by ZFMISC_1:6;
     hence thesis by Th88;
    end;
    assume a,b are_conjugated;
     then consider g such that A2: a |^ g = b by Th88;
        {b} = {a} |^ {g} by A2,Th44
         .= {a} |^ g by Def4;
   hence thesis by Th104;
  end;

theorem Th109:
 A,carr H1 are_conjugated implies
  ex H2 being strict Subgroup of G st the carrier of H2 = A
  proof assume A,carr H1 are_conjugated;
    then consider g such that A1: A = carr H1 |^ g by Def9;
       A = the carrier of H1 |^ g by A1,Def6;
   hence thesis;
  end;

definition let G,A;
 func con_class A -> Subset-Family of G equals
  :Def10:  {B : A,B are_conjugated};
 coherence
  proof set X = {B: A,B are_conjugated};
      X c= bool the carrier of G
     proof let x;
       assume x in X;
        then ex B st x = B & A,B are_conjugated;
      hence thesis;
     end;
   hence thesis by SETFAM_1:def 7;
  end;
end;

canceled;

theorem Th111:
 x in con_class A iff ex B st x = B & A,B are_conjugated
  proof
   thus x in con_class A implies ex B st x = B & A,B are_conjugated
    proof assume x in con_class A;
       then x in {B : A,B are_conjugated} by Def10;
     hence thesis;
    end;
    given B such that A1: x = B & A,B are_conjugated;
       x in {C : A,C are_conjugated} by A1;
   hence thesis by Def10;
  end;

canceled;

theorem Th113:
 A in con_class B iff A,B are_conjugated
  proof
   thus A in con_class B implies A,B are_conjugated
    proof assume A in con_class B;
      then ex C st A = C & B,C are_conjugated by Th111;
     hence thesis;
    end;
    assume A,B are_conjugated;
   hence thesis by Th111;
  end;

theorem
   A |^ g in con_class A
  proof A,A |^ g are_conjugated by Th104;
   hence thesis by Th111;
  end;

theorem
  A in con_class A by Th111;

theorem
   A in con_class B implies B in con_class A
  proof assume A in con_class B;
    then A,B are_conjugated by Th113;
   hence thesis by Th113;
  end;

theorem
   con_class A = con_class B iff con_class A meets con_class B
  proof
   thus con_class A = con_class B implies con_class A meets con_class B
    proof assume con_class A = con_class B;
      then A in con_class B & A in con_class A by Th111;
     hence thesis by XBOOLE_0:3;
    end;
    assume con_class A meets con_class B;
     then consider x such that A1: x in con_class A & x in
 con_class B by XBOOLE_0:3;
     reconsider x as Subset of G by A1;
   thus con_class A c= con_class B
    proof let y;
      assume y in con_class A;
       then consider C such that A2: C = y & A,C are_conjugated by Th111;
          x,A are_conjugated & x,B are_conjugated by A1,Th113;
        then x,C are_conjugated & B,x are_conjugated by A2,Th107;
        then B,C are_conjugated by Th107;
     hence thesis by A2,Th111;
    end;
   let y;
    assume y in con_class B;
     then consider C such that A3: C = y & B,C are_conjugated by Th111;
        x,B are_conjugated & x,A are_conjugated by A1,Th113;
      then A,x are_conjugated & x,C are_conjugated by A3,Th107;
      then A,C are_conjugated by Th107;
   hence thesis by A3,Th111;
  end;

theorem Th118:
 con_class{a} = {{b} : b in con_class a}
  proof set A = {{b} : b in con_class a};
   thus con_class{a} c= A
    proof let x;
      assume x in con_class{a};
       then consider B such that A1: x = B & {a},B are_conjugated by Th111;
       consider b such that A2: {a} |^ b = B by A1,Th104;
         A3: B = {a} |^ {b} by A2,Def4
            .= {a |^ b} by Th44;
          a,a |^ b are_conjugated by Th88;
        then a |^ b in con_class a by Th96;
     hence thesis by A1,A3;
    end;
   let x;
    assume x in A;
     then consider b such that A4: x = {b} & b in con_class a;
        b,a are_conjugated by A4,Th96;
      then {b},{a} are_conjugated by Th108;
   hence thesis by A4,Th113;
  end;

theorem
   G is finite implies con_class A is finite
  proof assume G is finite;
    then the carrier of G is finite by GROUP_1:def 13;
    then con_class A c= bool the carrier of G & bool the carrier of G is
finite
                                                     by FINSET_1:24;
   hence thesis by FINSET_1:13;
  end;

definition let G,H1,H2;
 pred H1,H2 are_conjugated means
  :Def11: ex g st the HGrStr of H1 = H2 |^ g;
 antonym H1,H2 are_not_conjugated;
end;

canceled;

theorem Th121:
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated iff ex g st H2 = H1 |^ g
  proof let H1,H2 be strict Subgroup of G;
   thus H1,H2 are_conjugated implies ex g st H2 = H1 |^ g
    proof given g such that A1: the HGrStr of H1 = H2 |^ g;
        H1 |^ g" = H2 by A1,Th74;
     hence thesis;
    end;
    given g such that A2: H2 = H1 |^ g;
       H1 = H2 |^ g" by A2,Th74;
   hence thesis by Def11;
  end;

theorem Th122:
 for H1 being strict Subgroup of G holds H1,H1 are_conjugated
  proof let H1 be strict Subgroup of G;
   take 1.G;
   thus thesis by Th73;
  end;

theorem Th123:
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated implies H2,H1 are_conjugated
  proof let H1,H2 be strict Subgroup of G;
   given g such that A1: the HGrStr of H1 = H2 |^ g;
      H2 = H1 |^ g" by A1,Th74;
   hence thesis by Def11;
  end;

definition let G; let H1,H2 be strict Subgroup of G;
 redefine pred H1,H2 are_conjugated;
 reflexivity by Th122;
 symmetry by Th123;
end;

theorem Th124:
 for H1,H2 being strict Subgroup of G holds
 H1,H2 are_conjugated & H2,H3 are_conjugated implies H1,H3 are_conjugated
  proof let H1,H2 be strict Subgroup of G;
   given g such that A1: the HGrStr of H1 = H2 |^ g;
    given h such that A2: the HGrStr of H2 = H3 |^ h;
       H1 = H3 |^ (h * g) by A1,A2,Th72;
   hence thesis by Def11;
  end;

reserve L for Subset of Subgroups G;

definition let G,H;
 func con_class H -> Subset of Subgroups G means
  :Def12: x in it iff
   ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated;
 existence
  proof
   defpred P[set] means
     ex H1 being strict Subgroup of G st $1 = H1 & H,H1 are_conjugated;
   consider L such that
    A1: x in L iff x in Subgroups G & P[x] from Subset_Ex;
   take L;
   let x;
   thus x in L implies
    ex H1 being strict Subgroup of G st x = H1 & H,H1 are_conjugated by A1;
    given H1 being strict Subgroup of G such that
    A2: x = H1 & H,H1 are_conjugated;
       x in Subgroups G by A2,Def1;
   hence thesis by A1,A2;
  end;
 uniqueness
  proof let A1,A2 be Subset of Subgroups G;
    defpred P[set] means
      ex H3 being strict Subgroup of G st $1 = H3 & H,H3 are_conjugated;
    assume A3: x in A1 iff P[x];
    assume A4: x in A2 iff P[x];
   thus thesis from Extensionality(A3,A4);
  end;
end;

canceled 2;

theorem Th127:
 x in con_class H implies x is strict Subgroup of G
  proof assume x in con_class H;
    then ex H1 being strict Subgroup of G st
 x = H1 & H,H1 are_conjugated by Def12;
   hence thesis;
  end;

theorem Th128:
 for H1,H2 being strict Subgroup of G holds
 H1 in con_class H2 iff H1,H2 are_conjugated
  proof let H1,H2 be strict Subgroup of G;
   thus H1 in con_class H2 implies H1,H2 are_conjugated
    proof assume H1 in con_class H2;
      then ex H3 being strict Subgroup of G st
 H1 = H3 & H2,H3 are_conjugated by Def12;
     hence thesis;
    end;
    assume H1,H2 are_conjugated;
   hence thesis by Def12;
  end;

theorem Th129:
 for H being strict Subgroup of G holds H |^ g in con_class H
  proof let H be strict Subgroup of G;
      H,H |^ g are_conjugated by Th121;
   hence thesis by Def12;
  end;

theorem Th130:
 for H being strict Subgroup of G holds H in con_class H
  proof let H be strict Subgroup of G;
      H,H are_conjugated;
   hence thesis by Def12;
  end;

theorem
   for H1,H2 being strict Subgroup of G holds
 H1 in con_class H2 implies H2 in con_class H1
  proof let H1,H2 be strict Subgroup of G;
   assume H1 in con_class H2;
    then H1,H2 are_conjugated by Th128;
   hence thesis by Th128;
  end;

theorem
   for H1,H2 being strict Subgroup of G holds
 con_class H1 = con_class H2 iff con_class H1 meets con_class H2
  proof let H1,H2 be strict Subgroup of G;
   thus con_class H1 = con_class H2 implies con_class H1 meets con_class H2
    proof assume con_class H1 = con_class H2;
      then H1 in con_class H2 & H1 in con_class H1 by Th130;
     hence thesis by XBOOLE_0:3;
    end;
    assume con_class H1 meets con_class H2;
     then consider x such that A1: x in con_class H1 & x in con_class H2
                                                               by XBOOLE_0:3;
     reconsider x as strict Subgroup of G by A1,Th127;
   thus con_class H1 c= con_class H2
    proof let y;
      assume y in con_class H1;
       then consider H3 being strict Subgroup of G such that
       A2: H3 = y & H1,H3 are_conjugated by Def12;
          x,H1 are_conjugated & x,H2 are_conjugated by A1,Th128;
        then x,H3 are_conjugated & H2,x are_conjugated by A2,Th124;
        then H2,H3 are_conjugated by Th124;
     hence thesis by A2,Def12;
    end;
   let y;
    assume y in con_class H2;
     then consider H3 being strict Subgroup of G such that
     A3: H3 = y & H2,H3 are_conjugated by Def12;
        x,H2 are_conjugated & x,H1 are_conjugated by A1,Th128;
      then H1,x are_conjugated & x,H3 are_conjugated by A3,Th124;
      then H1,H3 are_conjugated by Th124;
   hence thesis by A3,Def12;
  end;

theorem
   G is finite implies con_class H is finite
  proof assume G is finite;
    then Subgroups G is finite & con_class H c= Subgroups G by Th19;
   hence thesis by FINSET_1:13;
  end;

theorem Th134:
 for H1 being strict Subgroup of G holds
 H1,H2 are_conjugated iff carr H1,carr H2 are_conjugated
  proof let H1 be strict Subgroup of G;
   thus H1,H2 are_conjugated implies carr H1,carr H2 are_conjugated
    proof given a such that A1: the HGrStr of H1 = H2 |^ a;
        carr H1 = the carrier of H1 by GROUP_2:def 9;
      then carr H1 = carr H2 |^ a by A1,Def6;
     hence thesis by Def9;
    end;
    given a such that A2: carr H1 = carr H2 |^ a;
       the carrier of H1 = carr H2 |^ a by A2,GROUP_2:def 9
                      .= the carrier of H2 |^ a by Def6;
     then H1 = H2 |^ a by GROUP_2:68;
   hence thesis by Def11;
  end;

definition let G;
 let IT be Subgroup of G;
 attr IT is normal means
  :Def13: for a holds IT |^ a = the HGrStr of IT;
end;

definition let G;
 cluster strict normal Subgroup of G;
 existence
  proof for a holds (1).G |^ a = (1).G by Th80;
    then (1).G is normal by Def13;
   hence thesis;
  end;
end;

reserve N2 for normal Subgroup of G;

canceled 2;

theorem Th137:
 (1).G is normal & (Omega).G is normal
  proof
   thus for a being Element of G
   holds (1).G |^ a = the HGrStr of (1).G
    by Th80;
   thus for a being Element of G
   holds (Omega).G |^ a = the HGrStr of (Omega).G
    by Th82;
  end;

theorem
   for N1,N2 being strict normal Subgroup of G
 holds N1 /\ N2 is normal
  proof let N1,N2 be strict normal Subgroup of G;
   let a;
   thus (N1 /\ N2) |^ a = (N1 |^ a) /\ (N2 |^ a) by Th76
                     .= N1 /\ (N2 |^ a) by Def13
                     .= the HGrStr of (N1 /\ N2) by Def13;
  end;

theorem
   for H being strict Subgroup of G holds
 G is commutative Group implies H is normal
  proof let H be strict Subgroup of G;
   assume G is commutative Group;
   hence H |^ a = the HGrStr of H by Th86;
  end;

theorem Th140:
 H is normal Subgroup of G iff for a holds a * H = H * a
  proof
   thus H is normal Subgroup of G implies for a holds a * H = H * a
    proof assume A1: H is normal Subgroup of G;
     let a;
      A2: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9
                     .= the carrier of the HGrStr of H by A1,Def13
                     .= carr H by GROUP_2:def 9;
      A3: carr(H |^ a) = the carrier of H |^ a by GROUP_2:def 9
                       .= a" * H * a by Th71;
     thus a * H = a * carr(H |^ a) by A2,GROUP_2:def 13
               .= a * (a" * H) * a by A3,GROUP_2:39
               .= a * a" * H * a by GROUP_2:127
               .= 1.G * H * a by GROUP_1:def 5
               .= 1.G * (H * a) by GROUP_2:128
               .= H * a by GROUP_2:43;
    end;
   assume A4: for a holds a * H = H * a;
     H is normal
    proof
     let a;
        the carrier of H |^ a = a" * H * a by Th71
                           .= H * a" * a by A4
                           .= H * (a" * a) by GROUP_2:129
                           .= H * 1.G by GROUP_1:def 5
                           .= carr H by GROUP_2:132
                          .= the carrier of H by GROUP_2:def 9;
     hence thesis by GROUP_2:68;
    end;
   hence thesis;
  end;

theorem Th141:
 for H being Subgroup of G holds
 H is normal Subgroup of G iff for a holds a * H c= H * a
  proof let H be Subgroup of G;
   thus H is normal Subgroup of G implies for a holds a * H c= H * a by Th140
;
    assume A1: for a holds a * H c= H * a;
     A2: now let a;
         a" * H c= H * a" by A1;
       then a * (a" * H) c= a * (H * a") by Th5;
       then a * a" * H c= a * (H * a") by GROUP_2:127;
       then 1.G * H c= a * (H * a") by GROUP_1:def 5;
       then carr H c= a * (H * a") by GROUP_2:132;
       then carr H c= a * H * a" by GROUP_2:128;
       then carr H * a c= a * H * a" * a by Th5;
       then H * a c= a * H * a" * a by GROUP_2:def 14;
       then H * a c= a * H * (a" * a) by GROUP_2:40;
       then H * a c= a * H * 1.G by GROUP_1:def 5;
      hence H * a c= a * H by GROUP_2:43;
     end;
       now let a;
         a * H c= H * a & H * a c= a * H by A1,A2;
      hence a * H = H * a by XBOOLE_0:def 10;
     end;
   hence thesis by Th140;
  end;

theorem Th142:
 for H being Subgroup of G holds
 H is normal Subgroup of G iff for a holds H * a c= a * H
  proof let H be Subgroup of G;
   thus H is normal Subgroup of G implies for a holds H * a c= a * H by Th140
;
    assume A1: for a holds H * a c= a * H;
     A2: now let a;
         H * a" c= a" * H by A1;
       then a * (H * a") c= a * (a" * H) by Th5;
       then a * (H * a") c= a * a" * H by GROUP_2:127;
       then a * (H * a") c= 1.G * H by GROUP_1:def 5;
       then a * (H * a") c= carr H by GROUP_2:132;
       then a * H * a" c= carr H by GROUP_2:128;
       then a * H * a" * a c= carr H * a by Th5;
       then a * H * a" * a c= H * a by GROUP_2:def 14;
       then a * H * (a" * a) c= H * a by GROUP_2:40;
       then a * H * 1.G c= H * a by GROUP_1:def 5;
      hence a * H c= H * a by GROUP_2:43;
     end;
       now let a;
         a * H c= H * a & H * a c= a * H by A1,A2;
      hence a * H = H * a by XBOOLE_0:def 10;
     end;
   hence thesis by Th140;
  end;

theorem
   for H being Subgroup of G holds
 H is normal Subgroup of G iff for A holds A * H = H * A
  proof let H be Subgroup of G;
   thus H is normal Subgroup of G implies for A holds A * H = H * A
    proof assume A1: H is normal Subgroup of G;
     let A;
     thus A * H c= H * A
      proof let x;
        assume x in A * H;
         then consider a,h such that A2: x = a * h & a in A & h in H
                                                               by GROUP_2:114;
            x in a * H by A2,GROUP_2:125;
          then x in H * a by A1,Th140;
         then ex g st x = g * a & g in H by GROUP_2:126;
       hence thesis by A2,GROUP_2:115;
      end;
     let x;
      assume x in H * A;
       then consider h,a such that A3: x = h * a & h in H & a in A by GROUP_2:
115;
          x in H * a by A3,GROUP_2:126;
        then x in a * H by A1,Th140;
       then ex g st x = a * g & g in H by GROUP_2:125;
     hence thesis by A3,GROUP_2:114;
    end;
    assume A4: for A holds A * H = H * A;
       now let a;
      thus a * H = {a} * H by Th7
                .= H * {a} by A4
                .= H * a by Th8;
     end;
   hence thesis by Th140;
  end;

theorem
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a holds H is Subgroup of H |^ a
  proof let H be strict Subgroup of G;
   thus H is normal Subgroup of G implies for a holds H is Subgroup of H |^ a
    proof assume A1: H is normal Subgroup of G;
     let a;
        H |^ a = the HGrStr of H by A1,Def13;
     hence thesis by GROUP_2:63;
    end;
    assume A2: for a holds H is Subgroup of H |^ a;
       now let a;
A3:      H is Subgroup of H |^ a" by A2;
      A4: the carrier of H |^ a" = carr(H |^ a") by GROUP_2:def 9;
        H |^ a" * a = carr(H |^ a") * a by GROUP_2:def 14
                .= a"" * H * a" * a by A4,Th71
                .= a"" * H * (a" * a) by GROUP_2:40
                .= a"" * H * 1.G by GROUP_1:def 5
                .= a"" * H by GROUP_2:43
                .= a * H by GROUP_1:19;
      hence H * a c= a * H by A3,Th6;
     end;
   hence thesis by Th142;
  end;

theorem
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a holds H |^ a is Subgroup of H
  proof let H be strict Subgroup of G;
   thus H is normal Subgroup of G implies for a holds H |^ a is Subgroup of H
    proof assume A1: H is normal Subgroup of G;
     let a;
        H |^ a = the HGrStr of H by A1,Def13;
     hence thesis by GROUP_2:63;
    end;
    assume A2: for a holds H |^ a is Subgroup of H;
       now let a;
A3:      H |^ a" is Subgroup of H by A2;

      A4: the carrier of H |^ a" = carr(H |^ a") by GROUP_2:def 9;
        H |^ a" * a = carr(H |^ a") * a by GROUP_2:def 14
                .= a"" * H * a" * a by A4,Th71
                .= a"" * H * (a" * a) by GROUP_2:40
                .= a"" * H * 1.G by GROUP_1:def 5
                .= a"" * H by GROUP_2:43
                .= a * H by GROUP_1:19;
      hence a * H c= H * a by A3,Th6;
     end;
   hence thesis by Th141;
  end;

theorem
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff con_class H = {H}
  proof let H be strict Subgroup of G;
   thus H is normal Subgroup of G implies con_class H = {H}
    proof assume A1: H is normal Subgroup of G;
     thus con_class H c= {H}
      proof let x;
        assume x in con_class H;
         then consider H1 being strict Subgroup of G such that
         A2: x = H1 & H,H1 are_conjugated by Def12;
            ex g st H1 = H |^ g by A2,Th121;
          then x = H by A1,A2,Def13;
       hence thesis by TARSKI:def 1;
      end;
        H in con_class H by Th130;
     hence thesis by ZFMISC_1:37;
    end;
   assume A3: con_class H = {H};
     H is normal
   proof
    let a;
       H |^ a in con_class H by Th129;
    hence thesis by A3,TARSKI:def 1;
   end;
   hence thesis;
  end;

theorem
   for H being strict Subgroup of G holds
 H is normal Subgroup of G iff for a st a in H holds con_class a c= carr H
  proof let H be strict Subgroup of G;
   thus H is normal Subgroup of G implies
         for a st a in H holds con_class a c= carr H
    proof assume A1: H is normal Subgroup of G;
     let a;
      assume A2: a in H;
     let x;
      assume x in con_class a;
       then consider b such that A3: x = b & a,b are_conjugated by Th95;
       consider c such that A4: b = a |^ c by A3,Th88;
          x in H |^ c by A2,A3,A4,Th70;
        then x in H by A1,Def13;
     hence thesis by GROUP_2:88;
    end;
   assume A5: for a st a in H holds con_class a c= carr H;
     H is normal
   proof
    let a;
       H |^ a = H
     proof
      let b;
      thus b in H |^ a implies b in H
       proof assume b in H |^ a;
        then consider c such that A6: b = c |^ a & c in H by Th70;
           b in con_class c & con_class c c= carr H by A5,A6,Th97;
         hence thesis by GROUP_2:88;
       end;
      assume b in H;
       then con_class b c= carr H & b |^ a" in con_class b by A5,Th97;
       then b |^ a" in H by GROUP_2:88;
       then b |^ a" |^ a in H |^ a by Th70;
      hence thesis by Th30;
     end;
    hence H |^ a = the HGrStr of H;
   end;
   hence thesis;
  end;

Lm5:
 for N1 being strict normal Subgroup of G
 holds carr N1 * carr N2 c= carr N2 * carr N1
 proof let N1 be strict normal Subgroup of G;
  let x;
   assume x in carr N1 * carr N2;
    then consider a,b such that A1: x = a * b & a in carr N1 & b in carr N2
                                                                 by GROUP_2:12;
       a in N1 by A1,GROUP_2:88;
     then a |^ b in N1 |^ b by Th70;
     then a |^ b in the HGrStr of N1 by Def13;
     then A2: a |^ b in carr N1 by GROUP_2:88;
       b * (a |^ b) = b * (b" * (a * b)) by Th20
                .= a * b by Th1;
  hence thesis by A1,A2,GROUP_2:12;
 end;

theorem Th148:
 for N1,N2 being strict normal Subgroup of G
 holds carr N1 * carr N2 = carr N2 * carr N1
  proof let N1,N2 be strict normal Subgroup of G;
      carr N1 * carr N2 c= carr N2 * carr N1 &
    carr N2 * carr N1 c= carr N1 * carr N2 by Lm5;
   hence thesis by XBOOLE_0:def 10;
  end;

theorem
   for N1,N2 being strict normal Subgroup of G
 ex N being strict normal Subgroup of G
 st the carrier of N = carr N1 * carr N2
  proof let N1,N2 be strict normal Subgroup of G;
        set A = carr N1 * carr N2;
        set B = carr N1; set C = carr N2;
       carr N1 * carr N2 = carr N2 * carr N1 by Th148;
    then consider H being strict Subgroup of G such that
    A1: the carrier of H = A by GROUP_2:93;
     A2: carr H = A by A1,GROUP_2:def 9;
       now let a;
      thus a * H = a * A by A2,GROUP_2:def 13
                .= a * B * C by GROUP_2:35
                .= a * N1 * C by GROUP_2:def 13
                .= N1 * a * C by Th140
                .= B * a * C by GROUP_2:def 14
                .= B * (a * C) by GROUP_2:36
                .= B * (a * N2) by GROUP_2:def 13
                .= B * (N2 * a) by Th140
                .= B * (C * a) by GROUP_2:def 14
                .= A * a by GROUP_2:37
                .= H * a by A2,GROUP_2:def 14;
     end;
     then H is normal Subgroup of G by Th140;
   hence thesis by A1;
  end;

theorem
   for N being normal Subgroup of G holds
 Left_Cosets N = Right_Cosets N
  proof let N be normal Subgroup of G;
   thus Left_Cosets N c= Right_Cosets N
    proof let x;
      assume x in Left_Cosets N;
       then consider a such that A1: x = a * N by GROUP_2:def 15;
          x = N * a by A1,Th140;
     hence thesis by GROUP_2:def 16;
    end;
   let x;
    assume x in Right_Cosets N;
     then consider a such that A2: x = N * a by GROUP_2:def 16;
        x = a * N by A2,Th140;
   hence thesis by GROUP_2:def 15;
  end;

Lm6: for X being finite set st card X = 2 ex x,y st x <> y & X = {x,y}
 proof let X be finite set;
  assume A1: card X = 2;
then A2:   X <> {} by CARD_1:47;
    consider x being Element of X;
      {x} c= X by A1,CARD_1:47,ZFMISC_1:37;
    then card(X \ {x}) = card X - card{x} by CARD_2:63
                      .= 1 + 1 - 1 by A1,CARD_1:79
                      .= 1;
   then consider y such that A3: X \ {x} = {y} by CARD_2:60;
  take x,y;
      now assume x = y;
      then not x in {x} by A3,XBOOLE_0:def 4;
     hence contradiction by TARSKI:def 1;
    end;
  hence x <> y;
  thus X c= {x,y}
   proof let z be set;
     assume A4: z in X;
        now per cases;
       suppose z = x;
        hence thesis by TARSKI:def 2;
       suppose z <> x;
         then not z in {x} by TARSKI:def 1;
         then z in {y} by A3,A4,XBOOLE_0:def 4;
         then z = y by TARSKI:def 1;
       hence thesis by TARSKI:def 2;
      end;
    hence thesis;
   end;
  let z be set;
   assume z in {x,y};
    then A5: z = x or z = y by TARSKI:def 2;
      y in X \ {x} by A3,TARSKI:def 1;
  hence thesis by A2,A5,XBOOLE_0:def 4;
 end;

theorem
   for H being Subgroup of G holds
 Left_Cosets H is finite & index H = 2 implies H is normal Subgroup of G
  proof let H be Subgroup of G;
   assume that A1: Left_Cosets H is finite and A2: index H = 2;
    consider B being finite set such that
A3:     B = Left_Cosets H & index H = card B by A1,GROUP_2:176;
    consider C being finite set such that
A4:   C = Right_Cosets H & index H = card C by A1,GROUP_2:176;
    consider x,y such that A5: x <> y and A6: Left_Cosets H = {x,y}
                         by A2,A3,Lm6;
    consider z1,z2 being set such that A7: z1 <> z2 and
     A8: Right_Cosets H = {z1,z2} by A2,A4,Lm6;
     A9: carr H in Left_Cosets H & carr H in Right_Cosets H by GROUP_2:165;
     then {x,y} = {x,carr H} or {x,y} = {carr H,y} by A6,TARSKI:def 2;
    then consider z3 being set such that A10: {x,y} = {carr H,z3};
       {z1,z2} = {z1,carr H} or {z1,z2} = {carr H,z2} by A8,A9,TARSKI:def 2;
    then consider z4 being set such that A11: {z1,z2} = {carr H,z4};

     A12: union Left_Cosets H = the carrier of G &
         union Right_Cosets H = the carrier of G by GROUP_2:167;
     A13: union Left_Cosets H = carr H \/ z3 by A6,A10,ZFMISC_1:93;
       carr H misses z3
      proof assume A14: not thesis;

           z3 in Left_Cosets H by A6,A10,TARSKI:def 2;
        then A15: ex a st z3 = a * H by GROUP_2:def 15;
           carr H = 1.G * H by GROUP_2:132;
         then carr H = z3 by A14,A15,GROUP_2:138;
         then {x,y} = {carr H} by A10,ENUMSET1:69;
         then x = carr H & y = carr H by ZFMISC_1:8;
       hence thesis by A5;
      end;
     then A16: z3 = (the carrier of G) \ carr H by A12,A13,XBOOLE_1:88;
     A17: union Right_Cosets H = carr H \/ z4 by A8,A11,ZFMISC_1:93;
A18:     carr H misses z4
      proof assume A19: not thesis;

           z4 in Right_Cosets H by A8,A11,TARSKI:def 2;
        then A20: ex a st z4 = H * a by GROUP_2:def 16;
           carr H = H * 1.G by GROUP_2:132;
         then carr H = z4 by A19,A20,GROUP_2:144;
         then {z1,z2} = {carr H} by A11,ENUMSET1:69;
         then z1 = carr H & z2 = carr H by ZFMISC_1:8;
       hence thesis by A7;
      end;

       now let c;
         now per cases;
        suppose A21: c * H = carr H;
          then c in H by GROUP_2:136;
         hence c * H = H * c by A21,GROUP_2:142;
        suppose A22: c * H <> carr H;
          then not c in H by GROUP_2:136;
          then A23: H * c <> carr H by GROUP_2:142;
            c * H in Left_Cosets H & H * c in Right_Cosets H
                                                by GROUP_2:def 15,def 16;
          then c * H = z3 & H * c = z4 by A6,A8,A10,A11,A22,A23,TARSKI:def 2;
         hence c * H = H * c by A12,A16,A17,A18,XBOOLE_1:88;
       end;
      hence c * H = H * c;
     end;
   hence thesis by Th140;
  end;

definition let G; let A;
 func Normalizator A -> strict Subgroup of G means
  :Def14: the carrier of it = {h : A |^ h = A};
 existence
  proof set X = {h : A |^ h = A};
       X c= the carrier of G
      proof let x;
        assume x in X;
         then ex h st x = h & A |^ h = A;
       hence thesis;
      end;
    then reconsider X as Subset of G;
       A |^ 1.G = A by Th61;
     then A1: 1.G in X;
     A2: now let a,b;
       assume that A3: a in X and A4: b in X;
 A5:        ex g st a = g & A |^ g = A by A3;
           ex h st b = h & A |^ h = A by A4;
         then A |^ (a * b) = A by A5,Th56;
      hence a * b in X;
     end;
       now let a;
       assume a in X;
        then ex b st a = b & A |^ b = A;
         then A = A |^ a" by Th63;
      hence a" in X;
     end;
   hence thesis by A1,A2,GROUP_2:61;
  end;
 uniqueness by GROUP_2:68;
end;

canceled 2;

theorem Th154:
 x in Normalizator A iff ex h st x = h & A |^ h = A
  proof
   thus x in Normalizator A implies ex h st x = h & A |^ h = A
    proof assume x in Normalizator A;
       then x in the carrier of Normalizator A by RLVECT_1:def 1;
       then x in {h : A |^ h = A} by Def14;
     hence thesis;
    end;
    given h such that A1: x = h & A |^ h = A;
       x in {b : A |^ b = A} by A1;
     then x in the carrier of Normalizator A by Def14;
   hence thesis by RLVECT_1:def 1;
  end;

theorem Th155:
 Card con_class A = Index Normalizator A
  proof defpred P[set,set] means ex a st $1 = A |^ a & $2 = Normalizator A * a;
     A1: for x,y1,y2 st x in con_class A & P[x,y1] & P[x,y2] holds y1 = y2
      proof let x,y1,y2;
        assume x in con_class A;
        given a such that A2: x = A |^ a and A3: y1 = Normalizator A * a;
        given b such that A4: x = A |^ b and A5: y2 = Normalizator A * b;
           A = A |^ b |^ a" by A2,A4,Th63
          .= A |^ (b * a") by Th56;
         then b * a" in Normalizator A by Th154;
       hence thesis by A3,A5,GROUP_2:143;
      end;
     A6: for x st x in con_class A ex y st P[x,y]
      proof let x;
        assume x in con_class A;
         then consider B such that A7: x = B & A,B are_conjugated by Th111;
         consider g such that A8: B = A |^ g by A7,Th104;
         reconsider y = Normalizator A * g as set;
       take y;
       take g;
       thus thesis by A7,A8;
      end;
    consider f being Function such that A9: dom f = con_class A and
     A10: for x st x in con_class A holds P[x,f.x] from FuncEx(A1,A6);
     A11: rng f = Right_Cosets Normalizator A
      proof
       thus rng f c= Right_Cosets Normalizator A
        proof let x;
          assume x in rng f;
           then consider y such that A12: y in dom f & f.y = x
           by FUNCT_1:def 5;
              ex a st y = A |^ a & x = Normalizator A * a
              by A9,A10,A12;
         hence thesis by GROUP_2:def 16;
        end;
       let x;
        assume x in Right_Cosets Normalizator A;
         then consider a such that A13: x = Normalizator A * a by GROUP_2:def
16;
         set y = A |^ a;
            A,A |^ a are_conjugated by Th104;
          then A14: y in con_class A by Th111;
         then ex b st y = A |^ b & f.y = Normalizator A * b
                                                               by A10;
          then x = f.y by A1,A13,A14;
       hence thesis by A9,A14,FUNCT_1:def 5;
      end;
       f is one-to-one
      proof let x,y;
        assume that A15: x in dom f and A16: y in dom f and A17: f.x = f.y;
         consider a such that A18: x = A |^ a & f.x = Normalizator A * a
                                                           by A9,A10,A15;
         consider b such that A19: y = A |^ b & f.y = Normalizator A * b
                                                           by A9,A10,A16;
            b * a" in Normalizator A by A17,A18,A19,GROUP_2:143;
         then ex h st b * a" = h & A |^ h = A by Th154;
          then A = A |^ b |^ a" by Th56;
       hence thesis by A18,A19,Th63;
      end;
     then con_class A,Right_Cosets Normalizator A are_equipotent
     by A9,A11,WELLORD2:def 4;
   hence Card con_class A = Card Right_Cosets Normalizator A by CARD_1:21
                         .= Index Normalizator A by GROUP_2:175;
  end;

theorem
   con_class A is finite or Left_Cosets Normalizator A is finite implies
  ex C being finite set st C = con_class A & card C = index Normalizator A
   proof assume A1: con_class A is finite or
                   Left_Cosets Normalizator A is finite;
     A2: Card con_class A = Index Normalizator A by Th155
                        .= Card Left_Cosets Normalizator A by GROUP_2:175;
     then A3: con_class A,Left_Cosets Normalizator A are_equipotent
     by CARD_1:21;
     then con_class A is finite & Left_Cosets Normalizator A is finite
                                                               by A1,CARD_1:68;
     then consider B being finite set such that
A4:   B = Left_Cosets Normalizator A & index Normalizator A = card B
         by GROUP_2:def 18;
     reconsider C = con_class A as finite set by A1,A3,CARD_1:68;
    take C;
    thus C = con_class A;
    thus card C = index Normalizator A by A2,A4;
   end;

theorem Th157:
 Card con_class a = Index Normalizator{a}
  proof
    deffunc F(set) = {$1};
    consider f being Function such that A1: dom f = con_class a and
     A2: for x st x in con_class a holds f.x = F(x) from Lambda;
     A3: rng f = con_class{a}
      proof
       thus rng f c= con_class{a}
        proof let x;
          assume x in rng f;
           then consider y such that A4: y in dom f & f.y = x by FUNCT_1:def 5;
           reconsider y as Element of G by A1,A4;
              f.y = {y} by A1,A2,A4;
            then x in {{d} : d in con_class a} by A1,A4;
         hence thesis by Th118;
        end;
       let x;
        assume x in con_class{a};
          then x in {{b} : b in con_class a} by Th118;
         then consider b such that A5: x = {b} & b in con_class a;
            f.b = {b} by A2,A5;
       hence thesis by A1,A5,FUNCT_1:def 5;
      end;
       f is one-to-one
      proof let x,y;
        assume that A6: x in dom f & y in dom f and A7: f.x = f.y;
           f.x = {x} & f.y = {y} by A1,A2,A6;
       hence thesis by A7,ZFMISC_1:6;
      end;
     then con_class a,con_class{a} are_equipotent by A1,A3,WELLORD2:def 4;
   hence Card con_class a = Card con_class{a} by CARD_1:21
                         .= Index Normalizator{a} by Th155;
  end;

theorem
   con_class a is finite or Left_Cosets Normalizator{a} is finite implies
  ex C being finite set st C = con_class a & card C = index Normalizator{a}
   proof assume A1: con_class a is finite or
                   Left_Cosets Normalizator {a} is finite;
     A2: Card con_class a = Index Normalizator {a} by Th157
                        .= Card Left_Cosets Normalizator {a} by GROUP_2:175;
     then A3: con_class a,Left_Cosets Normalizator {a} are_equipotent
     by CARD_1:21;
     then con_class a is finite & Left_Cosets Normalizator {a} is finite
                                                               by A1,CARD_1:68;
     then consider B being finite set such that
A4:   B = Left_Cosets Normalizator {a} & index Normalizator {a} = card B
          by GROUP_2:def 18;
     reconsider C = con_class a as finite set by A1,A3,CARD_1:68;
    take C;
    thus C = con_class a;
    thus card C = index Normalizator {a} by A2,A4;
   end;

definition let G; let H;
 func Normalizator H -> strict Subgroup of G equals
  :Def15:  Normalizator carr H;
 correctness;
end;

canceled;

theorem Th160:
 for H being strict Subgroup of G
 holds x in Normalizator H iff ex h st x = h & H |^ h = H
  proof let H be strict Subgroup of G;
   thus x in Normalizator H implies ex h st x = h & H |^ h = H
    proof assume x in Normalizator H;
       then x in Normalizator carr H by Def15;
      then consider a such that A1: x = a & carr H |^ a = carr H
         by Th154;
         carr H = the carrier of H & the carrier of H |^ a = carr H |^ a
                                                           by Def6,GROUP_2:def
9;
       then H |^ a = H by A1,GROUP_2:68;
     hence thesis by A1;
    end;
    given h such that A2: x = h & H |^ h = H;
       carr H |^ h = the carrier of H by A2,Def6
                  .= carr H by GROUP_2:def 9;
     then x in Normalizator carr H by A2,Th154;
   hence thesis by Def15;
  end;

theorem Th161:
 for H being strict Subgroup of G holds
 Card con_class H = Index Normalizator H
  proof let H be strict Subgroup of G;
   defpred P[set,set] means
    ex H1 being strict Subgroup of G st $1 = H1 & $2 = carr H1;
     A1: for x,y1,y2 st x in con_class H & P[x,y1] & P[x,y2] holds y1 = y2;
     A2: for x st x in con_class H ex y st P[x,y]
      proof let x;
        assume x in con_class H;
          then reconsider H = x as strict Subgroup of G by Def1;
         reconsider y = carr H as set;
       take y;
       take H;
       thus thesis;
      end;
    consider f being Function such that A3: dom f = con_class H and
     A4: for x st x in con_class H holds P[x,f.x] from FuncEx(A1,A2);
     A5: rng f = con_class carr H
      proof
       thus rng f c= con_class carr H
        proof let x;
          assume x in rng f;
           then consider y such that A6: y in dom f & f.y = x by FUNCT_1:def 5;
           consider H1 being strict Subgroup of G such that
           A7: y = H1 & x = carr H1 by A3,A4,A6;
              H1,H are_conjugated by A3,A6,A7,Th128;
            then carr H1,carr H are_conjugated by Th134;
         hence thesis by A7,Th113;
        end;
       let x;
        assume x in con_class carr H;
         then consider B such that A8: B = x & carr H,B are_conjugated
                                                                      by Th111;
         consider H1 being strict Subgroup of G such that
         A9: the carrier of H1 = B by A8,Th109;
          A10: B = carr H1 by A9,GROUP_2:def 9;
          then H1,H are_conjugated by A8,Th134;
          then A11: H1 in con_class H by Th128;
         then ex H2 being strict Subgroup of G st
 H1 = H2 & f.H1 = carr H2 by A4;
       hence thesis by A3,A8,A10,A11,FUNCT_1:def 5;
      end;
       f is one-to-one
      proof let x,y;
        assume that A12: x in dom f and A13: y in dom f and A14: f.x = f.y;
         consider H1 being strict Subgroup of G such that
         A15: x = H1 & f.x = carr H1 by A3,A4,A12;
         consider H2 being strict Subgroup of G such that
         A16: y = H2 & f.y = carr H2 by A3,A4,A13;
            the carrier of H1 = carr H1 &
          the carrier of H2 = carr H2 by GROUP_2:def 9;
       hence thesis by A14,A15,A16,GROUP_2:68;
      end;
     then con_class H,con_class carr H are_equipotent
     by A3,A5,WELLORD2:def 4;
   hence Card con_class H = Card con_class carr H by CARD_1:21
                         .= Index Normalizator carr H by Th155
                         .= Index Normalizator H by Def15;
  end;

theorem
   for H being strict Subgroup of G holds
 con_class H is finite or Left_Cosets Normalizator H is finite implies
 ex C being finite set st C = con_class H & card C = index Normalizator H
   proof let H be strict Subgroup of G;
    assume A1: con_class H is finite or
                   Left_Cosets Normalizator H is finite;
     A2: Card con_class H = Index Normalizator H by Th161
                        .= Card Left_Cosets Normalizator H by GROUP_2:175;
     then A3: con_class H,Left_Cosets Normalizator H are_equipotent
     by CARD_1:21;
     then con_class H is finite & Left_Cosets Normalizator H is finite
                                                               by A1,CARD_1:68;
     then consider B being finite set such that
A4:      B = Left_Cosets Normalizator H & index Normalizator H = card B
       by GROUP_2:def 18;
     reconsider C = con_class H as finite set by A1,A3,CARD_1:68;
    take C;
    thus C = con_class H;
    thus card C = index Normalizator H by A2,A4;
   end;

theorem Th163:
 for G being strict Group, H being strict Subgroup of G
 holds H is normal Subgroup of G iff Normalizator H = G
  proof let G be strict Group, H be strict Subgroup of G;
   thus H is normal Subgroup of G implies Normalizator H = G
    proof assume A1: H is normal Subgroup of G;
        now let a be Element of G;
          H |^ a = H by A1,Def13;
       hence a in Normalizator H by Th160;
      end;
     hence thesis by GROUP_2:71;
    end;
   assume A2: Normalizator H = G;
     H is normal
   proof
    let a be Element of G;
       a in Normalizator H by A2,RLVECT_1:def 1;
    then ex b being Element of G
    st b = a & H |^ b = H by Th160;
    hence H |^ a = the HGrStr of H;
   end;
   hence thesis;
  end;

theorem
   for G being strict Group holds Normalizator (1).G = G
  proof let G be strict Group;
      (1).G is normal Subgroup of G by Th137;
   hence thesis by Th163;
  end;

theorem
   for G being strict Group holds Normalizator (Omega).G = G
  proof let G be strict Group;
      (Omega).G is normal Subgroup of G by Th137;
   hence thesis by Th163;
  end;

::
::  Auxiliary theorems.
::

theorem
   for X being finite set st card X = 2 ex x,y st x <> y & X = {x,y} by Lm6;

Back to top