The Mizar article:

Homomorphisms and Isomorphisms of Groups. Quotient Group

by
Wojciech A. Trybulec, and
Michal J. Trybulec

Received October 3, 1991

Copyright (c) 1991 Association of Mizar Users

MML identifier: GROUP_6
[ MML identifier index ]


environ

 vocabulary FUNCT_1, REALSET1, GROUP_2, GROUP_3, RLSUB_1, INT_1, BOOLE,
      RELAT_1, GROUP_1, RCOMP_1, SUBSET_1, GROUP_4, GROUP_5, VECTSP_1,
      NATTRA_1, FINSET_1, CARD_1, BINOP_1, QC_LANG1, ABSVALUE, WELLORD1,
      LATTICES, GROUP_6;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, STRUCT_0, CARD_1, FINSET_1, BINOP_1, REALSET1, INT_1,
      RLVECT_1, VECTSP_1, GROUP_1, GROUP_2, GROUP_3, NAT_1, GROUP_4, GROUP_5;
 constructors DOMAIN_1, BINOP_1, REALSET1, NAT_1, GROUP_4, GROUP_5, MEMBERED,
      PARTFUN1, RELAT_2, XBOOLE_0;
 clusters FUNCT_1, FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1,
      INT_1, FUNCT_2, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, VECTSP_1, STRUCT_0;
 theorems BINOP_1, CARD_1, CARD_2, FINSET_1, FUNCT_1, FUNCT_2, GROUP_1,
      GROUP_2, GROUP_3, GROUP_4, GROUP_5, TARSKI, ZFMISC_1, RLVECT_1, REALSET1,
      VECTSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1;
 schemes BINOP_1, COMPLSP1, FUNCT_1, FUNCT_2, DOMAIN_1, NAT_1;

begin

theorem Th1:
 for A,B being non empty set, f being Function of A,B holds
  f is one-to-one iff
   for a,b being Element of A st f.a = f.b holds a = b
  proof
   let A,B be non empty set;
   let f be Function of A,B;
   thus f is one-to-one implies
    for a,b being Element of A st f.a = f.b holds a = b
         by FUNCT_2:25;
      assume for a,b being Element of A st f.a = f.b holds a = b;
      then for a,b being set st a in A & b in A & f.a = f.b holds a = b;
      hence thesis by FUNCT_2:25;
  end;

definition let G be Group, A be Subgroup of G;
 redefine mode Subgroup of A -> Subgroup of G;
 coherence
 proof
  let H be Subgroup of A;
  thus thesis by GROUP_2:65;
 end;
end;

definition let G be Group;
 cluster (1).G -> normal;
 coherence by GROUP_3:137;
 cluster (Omega).G -> normal;
 coherence by GROUP_3:137;
end;

reserve n for Nat;
reserve i for Integer;
reserve G,H,I for Group;
reserve A,B for Subgroup of G;
reserve N for normal Subgroup of G;
reserve a,a1,a2,a3,b,b1 for Element of G;
reserve c,d for Element of H;
reserve f for Function of the carrier of G, the carrier of H;
reserve x,y,y1,y2,z for set;
reserve A1,A2 for Subset of G;

theorem Th2:
 for X being Subgroup of A, x being Element of A st x = a holds
  x * X = a * (X qua Subgroup of G) & X * x = (X qua Subgroup of G) * a
 proof let X be Subgroup of A, x be Element of A;
   assume A1: x = a;
    set I = X qua Subgroup of G;
  thus x * X c= a * I
   proof let y;
     assume y in x * X;
      then consider g being Element of A such that
         A2: y = x * g & g in X by GROUP_2:125;
      reconsider h = g as Element of G by GROUP_2:51;
         a * h = x * g by A1,GROUP_2:52;
    hence thesis by A2,GROUP_2:125;
   end;
  thus a * I c= x * X
   proof let y;
     assume y in a * I;
      then consider b such that A3: y = a * b & b in X by GROUP_2:125;
      reconsider c = b as Element of X by A3,RLVECT_1:def 1;
      reconsider c as Element of A by GROUP_2:51;
         a * b = x * c by A1,GROUP_2:52;
    hence thesis by A3,GROUP_2:125;
   end;
  thus X * x c= I * a
   proof let y;
     assume y in X * x;
      then consider g being Element of A such that
        A4: y = g * x & g in X by GROUP_2:126;
      reconsider h = g as Element of G by GROUP_2:51;
         h * a = g * x by A1,GROUP_2:52;
    hence thesis by A4,GROUP_2:126;
   end;
  thus I * a c= X * x
   proof let y;
     assume y in I * a;
      then consider b such that A5: y = b * a & b in X by GROUP_2:126;
      reconsider c = b as Element of X by A5,RLVECT_1:def 1;
      reconsider c as Element of A by GROUP_2:51;
         b * a = c * x by A1,GROUP_2:52;
    hence thesis by A5,GROUP_2:126;
   end;
 end;

theorem
   for X,Y being Subgroup of A holds
  (X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y
 proof let X,Y be Subgroup of A;
    A1: the carrier of X /\ Y = (carr X) /\ (carr Y) &
     the carrier of (X qua Subgroup of G) /\ (Y qua Subgroup of G) =
     (carr (X qua Subgroup of G)) /\ (carr (Y qua Subgroup of G)) &
     carr X = the carrier of X & the carrier of Y = carr Y &
     carr (X qua Subgroup of G) = the carrier of X &
     the carrier of Y = carr (Y qua Subgroup of G)
                                      by GROUP_2:def 9,def 10;
    reconsider Z = X /\ Y as Subgroup of G by GROUP_2:65;
       (X qua Subgroup of G) /\ (Y qua Subgroup of G) = Z by A1,GROUP_2:97;
  hence thesis;
 end;

theorem Th4:
 a * b * a" = b |^ a" & a * (b * a") = b |^ a"
  proof
   thus a * b * a" = a"" * b * a" by GROUP_1:19
                  .= b |^ a" by GROUP_3:def 2;
   hence thesis by VECTSP_1:def 16;
  end;

canceled;

theorem Th6:
 a * A * A = a * A & a * (A * A) = a * A &
 A * A * a = A * a & A * (A * a) = A *a
  proof
   thus a * A * A = a * (A * A) by GROUP_4:60
                 .= a * carr A by GROUP_4:58
                 .= a * A by GROUP_2:def 13;
   hence a * (A * A) = a * A by GROUP_4:60;
   thus A * A * a = carr A * a by GROUP_4:58
                 .= A * a by GROUP_2:def 14;
   hence thesis by GROUP_4:61;
  end;

theorem Th7:
 for G being Group, A1 being Subset of G holds
 A1 = {[.a,b.] where a is Element of G,
                     b is Element of G : not contradiction}
  implies G` = gr A1
  proof let G be Group, A1 be Subset of G;
   assume A1: A1 =
    {[.a,b.] where a is Element of G,
                   b is Element of G : not contradiction};
      A1 = commutators G
     proof
      thus A1 c= commutators G
       proof let x;
         assume x in A1;
          then ex a,b being Element of G st x = [.a,b.] by A1;
        hence thesis by GROUP_5:65;
       end;
      let x;
       assume x in commutators G;
        then ex a,b being Element of G st x = [.a,b.]
           by GROUP_5:65;
      hence thesis by A1;
     end;
   hence thesis by GROUP_5:82;
  end;

theorem Th8:
 for G being strict Group, B being strict Subgroup of G holds
 G` is Subgroup of B iff
    for a,b being Element of G holds [.a,b.] in B
  proof let G be strict Group, B be strict Subgroup of G;
   thus G` is Subgroup of B implies
    for a,b being Element of G holds [.a,b.] in B
    proof assume A1: G` is Subgroup of B;
     let a,b be Element of G;
        [.a,b.] in G` by GROUP_5:84;
     hence thesis by A1,GROUP_2:49;
    end;
    assume A2: for a,b being Element of G holds [.a,b.] in B;
     defpred P[set,set] means not contradiction;
     deffunc F(Element of G,Element of G) =
       [.$1,$2.];
     reconsider X =
     {F(a,b) where a is Element of G,
                    b is Element of G : P[a,b]}
 as Subset of G from SubsetFD2;
        X c= the carrier of B
       proof let x;
         assume x in X;
          then ex a,b being Element of G st x = [.a,b.];
           then x in B by A2;
        hence thesis by RLVECT_1:def 1;
       end;
      then gr X is Subgroup of B by GROUP_4:def 5;
   hence thesis by Th7;
  end;

theorem Th9:
 for N being normal Subgroup of G holds
 N is Subgroup of B implies N is normal Subgroup of B
  proof let N be normal Subgroup of G;
   assume N is Subgroup of B;
    then reconsider N' = N as Subgroup of B;
        now let n be Element of B;
       thus n * N' c= N' * n
        proof let x;
          assume x in n * N';
           then consider a being Element of B such that
            A1: x = n * a and A2: a in N' by GROUP_2:125;
           reconsider a' = a, n' = n as Element of G
                by GROUP_2:51;
              x = n' * a' by A1,GROUP_2:52;
            then x in n' * N & n' * N c= N * n' by A2,GROUP_2:125,GROUP_3:141;
            then consider a1 such that A3: x = a1 * n' and A4: a1 in N
                                                               by GROUP_2:126;
              a1 in N' by A4;
            then a1 in B by GROUP_2:49;
           then reconsider a1' = a1 as Element of B
                  by RLVECT_1:def 1;
              x = a1' * n by A3,GROUP_2:52;
         hence thesis by A4,GROUP_2:126;
        end;
      end;
     hence thesis by GROUP_3:141;
  end;

definition let G,B; let M be normal Subgroup of G;
 assume A1: the HGrStr of M is Subgroup of B;
 func (B,M)`*` -> strict normal Subgroup of B equals
  :Def1:  the HGrStr of M;
 coherence
  proof
   reconsider x = the HGrStr of M as Subgroup of G by A1;
     now let a;
A2:  carr x = the carrier of M by GROUP_2:def 9
           .= carr M by GROUP_2:def 9;
    thus a * x = a * carr x by GROUP_2:def 13
              .= a * M by A2,GROUP_2:def 13
              .= M * a by GROUP_3:140
              .= carr(M) * a by GROUP_2:def 14
              .= x * a by A2,GROUP_2:def 14;
   end;
   then x is normal Subgroup of G by GROUP_3:140;
   hence thesis by A1,Th9;
  end;
 correctness;
end;

theorem Th10:
 B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B
  proof
   thus
   B /\ N is normal Subgroup of B
    proof reconsider A = B /\ N as Subgroup of B by GROUP_2:106;
        now let b be Element of B;
       thus b * A c= A * b
        proof let x;
          assume x in b * A;
           then consider a being Element of B such that
           A1: x = b * a and
            A2: a in A by GROUP_2:125;
            A3: a in N by A2,GROUP_2:99;
           reconsider a' = a, b' = b as Element of G
             by GROUP_2:51;
              x = b' * a' by A1,GROUP_2:52;
            then x in b' * N & b' * N c= N * b' by A3,GROUP_2:125,GROUP_3:141;
            then consider b1 such that A4: x = b1 * b' and A5: b1 in N
                                                              by GROUP_2:126;
           reconsider x' = x as Element of B by A1;
           reconsider x'' = x as Element of G by A4;
              b1 = x'' * b'" & b'" = b" by A4,GROUP_1:22,GROUP_2:57;
            then A6:b1 = x' * b" by GROUP_2:52;
            then A7: b1 in B by RLVECT_1:def 1;
           reconsider b1' = b1 as Element of B by A6;
              b1' * b = x & b1' in A by A4,A5,A7,GROUP_2:52,99;
         hence thesis by GROUP_2:126;
        end;
      end;
     hence thesis by GROUP_3:141;
    end;
   hence thesis;
  end;

definition let G,B; let N be normal Subgroup of G;
 redefine func B /\ N -> strict normal Subgroup of B;
 coherence by Th10;
end;

definition let G; let N be normal Subgroup of G; let B;
 redefine func N /\ B -> strict normal Subgroup of B;
 coherence by Th10;
end;

definition let G be non empty 1-sorted;
  redefine attr G is trivial means :Def2:
  ex x st the carrier of G = {x};
 compatibility
  proof
   hereby assume A1: G is trivial;
    consider y being Element of G;
      for x holds x in the carrier of G iff x = y by A1,REALSET1:def 20;
    then the carrier of G = {y} by TARSKI:def 1;
    hence ex x st the carrier of G = {x};
   end;
   given x such that
A2:   the carrier of G = {x};
     now let a,b be Element of G;
    thus a = x by A2,TARSKI:def 1 .= b by A2,TARSKI:def 1;
   end;
   hence thesis by REALSET1:def 20;
  end;
end;

definition
 cluster trivial Group;
 existence
  proof consider G;
   take (1).G;
      the carrier of (1).G = {1.G} by GROUP_2:def 7;
   hence thesis by Def2;
  end;
end;

theorem Th11:
 (1).G is trivial
  proof
     the carrier of (1).G = {1.G} by GROUP_2:def 7;
   hence thesis by Def2;
  end;

theorem Th12:
 G is trivial iff ord G = 1 & G is finite
  proof
   thus G is trivial implies ord G = 1 & G is finite
    proof
     given x such that A1: the carrier of G = {x};
     G is finite by A1,GROUP_1:def 13;
      then ex B being finite set st B = the carrier of G & ord G = card B
              by GROUP_1:def 14;
     hence thesis by A1,CARD_1:79,GROUP_1:def 13;
    end;
   assume
A2: ord G = 1 & G is finite;
    then consider c being finite set such that
A3:   c = the carrier of G & ord G = card c by GROUP_1:def 14;
   thus ex x st the carrier of G = {x} by A2,A3,CARD_2:60;
  end;

theorem Th13:
 for G being strict Group holds
 G is trivial implies (1).G = G
  proof let G be strict Group;
   assume G is trivial;
   then A1: ord G = 1 & G is finite by Th12;
   then ord G = ord (1).G by GROUP_2:81;
   hence G = (1).G by A1,GROUP_2:85;
  end;

definition let G,N;
 func Cosets N -> set equals
  :Def3:  Left_Cosets N;
 coherence;
end;

definition let G,N;
 cluster Cosets N -> non empty;
 coherence
  proof
      Cosets N = Left_Cosets N by Def3;
   hence thesis by GROUP_2:165;
  end;
end;

theorem Th14:
 for N being normal Subgroup of G holds
 Cosets N = Left_Cosets N & Cosets N = Right_Cosets N
  proof let N be normal Subgroup of G;
   thus Cosets N = Left_Cosets N by Def3;
   hence thesis by GROUP_3:150;
  end;

theorem Th15:
 for N being normal Subgroup of G holds
 x in Cosets N implies ex a st x = a * N & x = N * a
  proof let N be normal Subgroup of G;
   assume x in Cosets N;
   then x in Left_Cosets N by Def3;
   then consider a such that A1: x = a * N by GROUP_2:def 15;
     x = N * a by A1,GROUP_3:140;
   hence thesis by A1;
  end;

theorem Th16:
 for N being normal Subgroup of G holds
 a * N in Cosets N & N * a in Cosets N
  proof let N be normal Subgroup of G;
A1: a * N in Left_Cosets N by GROUP_2:def 15;
   N * a in Right_Cosets N by GROUP_2:def 16;
   hence thesis by A1,Th14;
  end;

theorem Th17:
 for N being normal Subgroup of G holds
 x in Cosets N implies x is Subset of G
  proof let N be normal Subgroup of G;
   assume x in Cosets N;
   then ex a st x = a * N & x = N * a by Th15;
   hence thesis;
  end;

theorem Th18:
 for N being normal Subgroup of G holds
 A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N
  proof let N be normal Subgroup of G;
   assume A1: A1 in Cosets N & A2 in Cosets N;
   then consider a such that A2: A1 = a * N & A1 = N * a by Th15;
   consider b such that A3: A2 = b * N & A2 = N * b by A1,Th15;
     A1 * A2 = a * (N * (b * N)) by A2,A3,GROUP_3:11
          .= a * (b * N * N) by A3,GROUP_3:15
          .= a * (b * (N * N)) by GROUP_4:60
          .= a * (b * carr N) by GROUP_4:58
          .= a * (b * N) by GROUP_2:def 13
          .= a * b * N by GROUP_2:127;
   then A1 * A2 in Left_Cosets N by GROUP_2:def 15;
   hence thesis by Th14;
  end;

definition let G; let N be normal Subgroup of G;
 func CosOp N -> BinOp of Cosets N means
  :Def4: for W1,W2 being Element of Cosets N
       for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2;
 existence
  proof
    defpred P[Element of Cosets N,Element of Cosets N,set] means
      for A1,A2 st $1 = A1 & $2 = A2 holds $3 = A1 * A2;
    A1: for W1,W2 being Element of Cosets N
     ex V being Element of Cosets N st P[W1,W2,V]
     proof let W1,W2 be Element of Cosets N;
        reconsider A1 = W1, A2 = W2 as Subset of G by Th17;
       reconsider C = A1 * A2 as Element of Cosets N by Th18;
      take C;
      thus thesis;
     end;
   thus ex B being BinOp of Cosets N st
   for W1,W2 being Element of Cosets N holds
   P[W1,W2,B.(W1,W2)] from BinOpEx(A1);
  end;
 uniqueness
  proof let o1,o2 be BinOp of Cosets N;
    assume A2: for W1,W2 being Element of Cosets N
     for A1,A2 st W1 = A1 & W2 = A2 holds o1.(W1,W2) = A1 * A2;
    assume A3: for W1,W2 being Element of Cosets N
     for A1,A2 st W1 = A1 & W2 = A2 holds o2.(W1,W2) = A1 * A2;
       now let x,y be set;
       assume A4: x in Cosets N & y in Cosets N;
        then reconsider W = x, V = y as Element of Cosets N;
        reconsider A1 = x, A2 = y as Subset of G by A4,Th17;
           o1.(W,V) = A1 * A2 & o2.(W,V) = A1 * A2 by A2,A3;
      then o1.(x,y) = o2.(x,y) & o1. [x,y] = o1.(x,y) & o2. [x,y] = o2.(x,y)
                                                          by BINOP_1:def 1;
      hence o1. [x,y] = o2. [x,y];
     end;
   hence thesis by FUNCT_2:118;
  end;
end;

definition let G; let N be normal Subgroup of G;
 func G./.N -> HGrStr equals
  :Def5:  HGrStr (# Cosets N, CosOp N #);
 correctness;
end;

definition let G; let N be normal Subgroup of G;
 cluster G./.N -> strict non empty;
 coherence
  proof
      G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
   hence G./.N is strict & the carrier of G./.N is non empty;
  end;
end;

canceled 3;

theorem Th22:
 for N being normal Subgroup of G holds
 the carrier of G./.N = Cosets N
  proof let N be normal Subgroup of G;
     G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
   hence thesis;
  end;

theorem Th23:
 for N being normal Subgroup of G holds
 the mult of G./.N = CosOp N
  proof let N be normal Subgroup of G;
     G./.N = HGrStr (# Cosets N, CosOp N #) by Def5;
   hence thesis;
  end;

reserve N for normal Subgroup of G;
reserve S,T1,T2 for Element of G./.N;

definition
 let G,N,S;
  func @S -> Subset of G equals :Def6:  S;
 coherence
  proof
     S is Element of Cosets N by Th22;
   hence thesis by Th17;
  end;
end;

theorem Th24:
 for N being normal Subgroup of G, T1,T2 being Element of G./.N
 holds @T1 * @T2 = T1 * T2
  proof
   let N be normal Subgroup of G, T1,T2 be Element of G./.N;
   reconsider S1 = T1 as Element of Cosets N by Th22;
   reconsider S2 = T2 as Element of Cosets N by Th22;
     S1 = @T1 & S2 = @T2 by Def6;
   hence @T1 * @T2 = (CosOp N).(T1,T2) by Def4
                  .= (the mult of G./.N).(T1,T2) by Th23
                  .= T1 * T2 by VECTSP_1:def 10;
  end;

theorem Th25:
 @(T1 * T2) = @T1 * @T2
  proof
   thus @(T1 * T2) = T1 * T2 by Def6
                  .= @T1 * @T2 by Th24;
  end;

definition let G; let N be normal Subgroup of G;
 cluster G./.N -> associative Group-like;
 coherence
  proof A1: the carrier of G./.N = Cosets N by Th22;
     G./.N is associative Group-like
   proof
   thus for f,g,h being Element of G./.N
      holds f * (g * h) = f * g * h
    proof let f,g,h be Element of G./.N;
      consider a such that A2: f = a * N & f = N * a by A1,Th15;
      consider c being Element of G such that
       A3: h = c * N & h = N * c by A1,Th15;
       A4: @f = f & @g = g & @h = h by Def6;
     thus f * (g * h) = @f * @(g * h) by Th24
                     .= (a * N) * (@g * @h) by A2,A4,Th25
                     .= @f * @g * (c * N) by A2,A3,A4,GROUP_2:14
                     .= @(f * g) * @h by A3,A4,Th25
                     .= f * g * h by Th24;
    end;
     A5: carr N in Left_Cosets N & Cosets N = Left_Cosets N
                                                by Th14,GROUP_2:165;
    then reconsider e = carr N as Element of G./.N by Th22;
   take e;
   let h be Element of G./.N;
    consider a such that A6: h = a * N & h = N * a by A1,Th15;
     A7: @h = h & @e = e by Def6;
   thus h * e = @h * @e by Th24
             .= (a * N) * N by A6,A7,GROUP_2:def 11
             .= a * (N * N) by GROUP_4:60
             .= a * carr N by GROUP_4:58
             .= h by A6,GROUP_2:def 13;
   thus e * h = @e * @h by Th24
             .= N * (N * a) by A6,A7,GROUP_2:def 12
             .= N * N * a by GROUP_4:61
             .= carr N * a by GROUP_4:58
             .= h by A6,GROUP_2:def 14;
    reconsider g = a" * N as Element of G./.N by A1,A5,GROUP_2:
def 15;
     A8: @g = g by Def6;
   take g;
   thus h * g = N * a * (a" * N) by A6,A7,A8,Th24
             .= N * a * a" * N by GROUP_3:10
             .= N * (a * a") * N by GROUP_2:129
             .= N * 1.G * N by GROUP_1:def 5
             .= carr N * N by GROUP_2:132
             .= carr N * carr N by GROUP_2:def 11
             .= e by GROUP_2:91;
   thus g * h = @g * @h by Th24
             .= a" * N * a * N by A6,A7,A8,GROUP_3:10
             .= a" * (N * a) * N by GROUP_2:128
             .= a" * (a * N) * N by GROUP_3:140
             .= a" * a * N * N by GROUP_2:127
             .= 1.G * N * N by GROUP_1:def 5
             .= 1.G * (N * N) by GROUP_4:60
             .= 1.G * carr N by GROUP_4:58
             .= e by GROUP_2:43;
   end;
   hence thesis;
  end;
end;

theorem Th26:
 for N being normal Subgroup of G, S being Element of G./.N
 ex a st S = a * N & S = N * a
  proof let N be normal Subgroup of G, S be Element of G./.N;
      S in the carrier of G./.N & the carrier of G./.N = Cosets N by Th22;
   hence thesis by Th15;
  end;

theorem Th27:
 N * a is Element of G./.N &
 a * N is Element of G./.N &
  carr N is Element of G./.N
   proof N * a in Cosets N & a * N in
 Cosets N & Cosets N = the carrier of G./.N &
         carr N in Left_Cosets N & Cosets N = Left_Cosets N
     by Th14,Th16,Th22,GROUP_2:165;
    hence thesis;
   end;

theorem Th28:
 for N being normal Subgroup of G holds
 x in G./.N iff ex a st x = a * N & x = N * a
  proof let N be normal Subgroup of G;
   thus x in G./.N implies ex a st x = a * N & x = N * a
    proof assume x in G./.N;
      then x is Element of G./.N by RLVECT_1:def 1;
     hence thesis by Th26;
    end;
    given a such that A1: x = a * N & x = N * a;
       x is Element of G./.N by A1,Th27;
   hence thesis by RLVECT_1:def 1;
  end;

theorem Th29:
 for N being normal Subgroup of G holds
 1.(G./.N) = carr N
  proof let N be normal Subgroup of G;
   reconsider e = carr N as Element of G./.N by Th27;
     A1: the carrier of G./.N = Cosets N by Th22;
      now let h be Element of G./.N;
      consider a such that A2: h = a * N & h = N * a by A1,Th15;
       A3: @h = h & @e = e by Def6;
     thus h * e = @h * @e by Th24
               .= (a * N) * N by A2,A3,GROUP_2:def 11
               .= a * (N * N) by GROUP_4:60
               .= a * carr N by GROUP_4:58
               .= h by A2,GROUP_2:def 13;
     thus e * h = @e * @h by Th24
               .= N * (N * a) by A2,A3,GROUP_2:def 12
               .= N * N * a by GROUP_4:61
               .= carr N * a by GROUP_4:58
               .= h by A2,GROUP_2:def 14;
    end;
   hence thesis by GROUP_1:10;
  end;

theorem Th30:
 for N being normal Subgroup of G, S being Element of G./.N
 holds S = a * N implies S" = a" * N
  proof let N be normal Subgroup of G, S be Element of G./.N;
    assume A1: S = a * N;
    reconsider g = a" * N as Element of G./.N by Th27;
     A2: @g = g by Def6;
     A3: @S = S by Def6;
     A4: S * g = @S * @g by Th24
              .= N * a * (a" * N) by A1,A2,A3,GROUP_3:140
              .= N * a * a" * N by GROUP_3:10
              .= N * (a * a") * N by GROUP_2:129
              .= N * 1.G * N by GROUP_1:def 5
              .= carr N * N by GROUP_2:132
              .= carr N * carr N by GROUP_2:def 11
              .= carr N by GROUP_2:91;
     A5: g * S = @g * @S by Th24
              .= a" * N * a * N by A1,A2,A3,GROUP_3:10
              .= a" * (N * a) * N by GROUP_2:128
              .= a" * (a * N) * N by GROUP_3:140
              .= a" * a * N * N by GROUP_2:127
              .= 1.G * N * N by GROUP_1:def 5
              .= 1.G * (N * N) by GROUP_4:60
              .= 1.G * carr N by GROUP_4:58
              .= carr N by GROUP_2:43;
       1.(G./.N) = carr N by Th29;
   hence thesis by A4,A5,GROUP_1:def 5;
  end;

theorem Th31:
 for N being normal Subgroup of G holds
 Left_Cosets N is finite implies G./.N is finite
  proof let N be normal Subgroup of G;
   assume Left_Cosets N is finite;
    then Cosets N is finite by Th14;
    then the carrier of G./.N is finite by Th22;
   hence thesis by GROUP_1:def 13;
  end;

theorem
   for N being normal Subgroup of G holds
 Ord(G./.N) = Index N
  proof let N be normal Subgroup of G;
   thus Ord(G./.N) = Card(the carrier of G./.N) by GROUP_1:def 12
                 .= Card Cosets N by Th22
                 .= Card Left_Cosets N by Th14
                 .= Index N by GROUP_2:175;
  end;

theorem
   for N being normal Subgroup of G holds
 Left_Cosets N is finite implies ord(G./.N) = index N
  proof let N be normal Subgroup of G;
   assume A1: Left_Cosets N is finite;
    then reconsider LC = Left_Cosets N as finite set;
A2:  Cosets N = LC by Th14;
A3: G./.N is finite by A1,Th31;
    then reconsider GN = the carrier of G./.N as finite set by GROUP_1:def 13;
   thus ord(G./.N) = card GN by A3,GROUP_1:def 14
                  .= card LC by A2,Th22
                  .= index N by GROUP_2:def 18;
  end;

theorem Th34:
 for M being strict normal Subgroup of G holds
 M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M
  proof let M be strict normal Subgroup of G;
   assume A1: M is Subgroup of B;
    set I = B./.(B,M)`*`; set J = (B,M)`*`;
     A2: the carrier of I c= the carrier of G./.M
      proof let x;
        assume A3: x in the carrier of I;
            the carrier of I = Cosets((B,M)`*`) by Th22;
         then consider a being Element of B such that
          A4: x = a * J & x = J * a by A3,Th15;
         reconsider b = a as Element of G by GROUP_2:51;
            J = M by A1,Def1;
          then a * J = b * M & J * a = M * b by Th2;
          then x in Cosets M & the carrier of G./.M = Cosets M by A4,Th16,Th22
;
       hence thesis;
      end;
    set g = the mult of I;
    set f = the mult of G./.M;
    set X = [: the carrier of I,the carrier of I :];
     A5: dom g = X & dom f = [: the carrier of G./.M,the carrier of G./.M :] &
     X c= [: the carrier of G./.M,the carrier of G./.M :]
                                            by A2,FUNCT_2:def 1,ZFMISC_1:119;
     then A6: dom g = dom f /\ X by XBOOLE_1:28;
       now let x;
       assume A7: x in dom g;
        then consider y,z such that A8: [y,z] = x by A5,ZFMISC_1:102;
         A9: y in the carrier of I & z in
 the carrier of I by A5,A7,A8,ZFMISC_1:106;
         A10: the carrier of I = Cosets((B,M)`*`) by Th22;
        then consider a being Element of B such that
        A11: y = a * J & y = J * a by A9,Th15;
        consider b being Element of B such that
        A12: z = b * J & z = J * b by A9,A10,Th15;
        reconsider W1 = y, W2 = z as Element of Cosets J by A11,A12,Th16;
         A13: the mult of I = CosOp J & the mult of G./.M = CosOp M by Th23;
         A14: g.x = g.(W1,W2) by A8,BINOP_1:def 1
               .= (a * J) * (J * b) by A11,A12,A13,Def4
               .= a * J * J * b by GROUP_3:12
               .= a * (J * J) * b by GROUP_4:60
               .= a * carr J * b by GROUP_4:58
               .= a * J * b by GROUP_2:def 13
               .= a * (J * b) by GROUP_2:128
               .= a * (b * J) by GROUP_3:140
               .= a * b * J by GROUP_2:127;
         reconsider a' = a, b' = b as Element of G
            by GROUP_2:51;
          A15: J = M by A1,Def1;
          then A16: y = a' * M & y = M * a' & z = b' * M & z = M * b' by A11,
A12,Th2;
         then reconsider V1 = y, V2 = z as Element of Cosets M by Th16;
          A17: f.x = f.(V1,V2) by A8,BINOP_1:def 1
                .= (a' * M) * (M * b') by A13,A16,Def4
               .= a' * M * M * b' by GROUP_3:12
               .= a' * (M * M) * b' by GROUP_4:60
               .= a' * carr M * b' by GROUP_4:58
               .= a' * M * b' by GROUP_2:def 13
               .= a' * (M * b') by GROUP_2:128
               .= a' * (b' * M) by GROUP_3:140
               .= a' * b' * M by GROUP_2:127;
            a' * b' = a * b by GROUP_2:52;
      hence g.x = f.x by A14,A15,A17,Th2;
     end;
     then g = f | X by A6,FUNCT_1:68;
   hence thesis by A2,GROUP_2:def 5;
  end;

theorem
   for N,M being strict normal Subgroup of G holds
 M is Subgroup of N implies N./.(N,M)`*` is normal Subgroup of G./.M
  proof let N,M be strict normal Subgroup of G;
   assume A1: M is Subgroup of N;
     then A2: (N,M)`*` = M by Def1;
    reconsider J = N./.(N,M)`*` as Subgroup of G./.M by A1,Th34;
    reconsider I = M as normal Subgroup of N by A2;
       now let S be Element of G./.M;
      thus S * J c= J * S
       proof let x;
         assume x in S * J;
          then consider T being Element of G./.M such that
           A3: x = S * T and A4: T in J by GROUP_2:125;
          consider a such that A5: S = a * M & S = M * a by Th26;
          consider c being Element of N such that
           A6: T = c * I & T = I * c by A2,A4,Th28;
          reconsider d = c as Element of G by GROUP_2:51;
          set e = a * (d * a");
           A7: c in N by RLVECT_1:def 1;
             e = d |^ a" by Th4;
           then e in N by A7,GROUP_5:3;
          then reconsider f = e as Element of N
             by RLVECT_1:def 1;
          reconsider V = I * f as Element of J by A2,Th27;
           A8: V in J by RLVECT_1:def 1;
          reconsider V as Element of G./.M by GROUP_2:51;
    A9: @S = S & @T = T & c * I = d * M & M * d = I * c & M * e = I * f &
              @V = V by Def6,Th2;
           then x = M * a * (M * d) by A3,A5,A6,Th24
            .= M * a * (M * d * 1.G) by GROUP_2:43
            .= M * a * (M * d * (a" * a)) by GROUP_1:def 5
            .= M * a * (M * (d * (a" * a))) by GROUP_2:129
            .= M * a * M * (d * (a" * a)) by GROUP_3:12
            .= M * (a * M) * (d * (a" * a)) by GROUP_3:15
            .= M * (M * a) * (d * (a" * a)) by GROUP_3:140
            .= M * ((M * a) * (d * (a" * a))) by GROUP_3:14
            .= M * (M * (a * (d * (a" * a)))) by GROUP_2:129
            .= M * (M * (a * (d * a" * a))) by VECTSP_1:def 16
            .= M * (M * (a * (d * a") * a)) by VECTSP_1:def 16
            .= M * (M * e * a) by GROUP_2:129
            .= M * (e * M * a) by GROUP_3:140
            .= M * (e * (M * a)) by GROUP_2:128
            .= M * e * (M * a) by GROUP_3:13
            .= V * S by A5,A9,Th24;
        hence x in J * S by A8,GROUP_2:126;
       end;
     end;
   hence thesis by GROUP_3:141;
  end;

theorem
   for G being strict Group, N be strict normal Subgroup of G holds
 G./.N is commutative Group iff G` is Subgroup of N
  proof let G be strict Group, N be strict normal Subgroup of G;
   thus G./.N is commutative Group implies G` is Subgroup of N
    proof assume A1: G./.N is commutative Group;
        now let a,b be Element of G;
        reconsider S = a * N,T = b * N as Element of G./.N
            by Th27;
           S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by Def6,Th30;
         then A2: S" * T" = (a" * N) * (b" * N) by Th24;
           S = @S & T = @T by Def6;
         then A3: S * T = (a * N) * (b * N) by Th24;
         A4: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6;
           [.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
         then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
              [.S,T.] = 1.(G./.N) & 1.(G./.N) = carr N by A1,A2,A3,A4,Th24,Th29
,GROUP_5:40;
         then carr N = (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:11
                   .= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:15
                   .= (a" * N) * (b" * N) * (a * (b * N * N)) by GROUP_3:140
                   .= (a" * N) * (b" * N) * (a * (b * N)) by Th6
                   .= (a" * N) * (b" * N) * (a * b * N) by GROUP_2:127
                   .= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:11
                   .= a" * (N * b" * N) * (a * b * N) by GROUP_3:15
                   .= a" * (b" * N * N) * (a * b * N) by GROUP_3:140
                   .= a" * (b" * N) * (a * b * N) by Th6
                   .= (a" * b" * N) * (a * b * N) by GROUP_2:127
                   .= (a" * b") * (N * (a * b * N)) by GROUP_3:11
                   .= (a" * b") * (N * (a * b) * N) by GROUP_3:15
                   .= (a" * b") * ((a * b) * N * N) by GROUP_3:140
                   .= (a" * b") * ((a * b) * N) by Th6
                   .= (a" * b") * (a * b) * N by GROUP_2:127
                   .= [.a,b.] * N by GROUP_5:19;
       hence [.a,b.] in N by GROUP_2:136;
      end;
     hence thesis by Th8;
    end;
    assume A5: G` is Subgroup of N;
       now let S,T be Element of G./.N;
       consider a being Element of G such that
       A6: S = a * N & S = N * a by Th26;
       consider b being Element of G such that
       A7: T = b * N & T = N * b by Th26;
          [.a,b.] in N by A5,Th8;
        then A8: carr N = [.a,b.] * N by GROUP_2:136
                   .= (a" * b") * (a * b) * N by GROUP_5:19
                   .= (a" * b") * ((a * b) * N) by GROUP_2:127
                   .= (a" * b") * ((a * b) * N * N) by Th6
                   .= (a" * b") * (N * (a * b) * N) by GROUP_3:140
                   .= (a" * b") * (N * (a * b * N)) by GROUP_3:15
                   .= (a" * b" * N) * (a * b * N) by GROUP_3:11
                   .= a" * (b" * N) * (a * b * N) by GROUP_2:127
                   .= a" * (b" * N * N) * (a * b * N) by Th6
                   .= a" * (N * b" * N) * (a * b * N) by GROUP_3:140
                   .= a" * (N * (b" * N)) * (a * b * N) by GROUP_3:15
                   .= (a" * N) * (b" * N) * (a * b * N) by GROUP_3:11
                   .= (a" * N) * (b" * N) * (a * (b * N)) by GROUP_2:127
                   .= (a" * N) * (b" * N) * (a * (b * N * N)) by Th6
                   .= (a" * N) * (b" * N) * (a * (N * b * N)) by GROUP_3:140
                   .= (a" * N) * (b" * N) * (a * (N * (b * N))) by GROUP_3:15
                   .= (a" * N) * (b" * N) * (a * N * (b * N)) by GROUP_3:11;
           S" = @(S") & T" = @(T") & S" = a" * N & T" = b" * N by A6,A7,Def6,
Th30
;
         then A9: S" * T" = (a" * N) * (b" * N) by Th24;
           S = @S & T = @T by Def6;
         then A10: S * T = (a * N) * (b * N) by A6,A7,Th24;
         A11: @(S" * T") = (S" * T") & @(S * T) = (S * T) by Def6;
           [.S,T.] = (S" * T") * (S * T) by GROUP_5:19;
         then [.S,T.] = (a" * N) * (b" * N) * ((a * N) * (b * N)) &
              1.(G./.N) = carr N by A9,A10,A11,Th24,Th29;
      hence [.S,T.] = 1.(G./.N) by A8;
     end;
   hence thesis by GROUP_5:40;
  end;

Lm1: (for a holds f.a = 1.H) implies f.(a * b) = f.a * f.b
 proof
  assume A1: for a holds f.a = 1.H;
  hence f.(a * b) = 1.H
                 .= 1.H * 1.H by GROUP_1:def 4
                 .= f.a * 1.H by A1
                 .= f.a * f.b by A1;
 end;

definition let G,H;
 mode Homomorphism of G,H ->
       Function of the carrier of G, the carrier of H means
 :Def7: it.(a * b) = it.a * it.b;
 existence
  proof
   deffunc F(Element of G) = 1.H;
   consider f such that A1: for a holds f.a = F(a) from LambdaD;
   take f;
   thus thesis by A1,Lm1;
  end;
end;

reserve g,h for Homomorphism of G,H;
reserve g1 for Homomorphism of H,G;
reserve h1 for Homomorphism of H,I;

canceled 3;

theorem Th40:
 g.(1.G) = 1.H
  proof g.(1.G) = g.(1.G * 1.G) by GROUP_1:def 4
               .= g.(1.G) * g.(1.G) by Def7;
   hence thesis by GROUP_1:15;
  end;

theorem Th41:
 g.(a") = (g.a)"
  proof g.(a") * g.a = g.(a" * a) by Def7
                    .= g.(1.G) by GROUP_1:def 5
                    .= 1.H by Th40;
   hence thesis by GROUP_1:20;
  end;

theorem Th42:
 g.(a |^ b) = (g.a) |^ (g.b)
  proof
   thus g.(a |^ b) = g.(b" * a * b) by GROUP_3:def 2
                 .= g.(b" * a) * g.b by Def7
                 .= g.(b") * g.a * g.b by Def7
                 .= (g.b)" * g.a * g.b by Th41
                 .= (g.a) |^ (g.b) by GROUP_3:def 2;
  end;

theorem Th43:
 g. [.a,b.] = [.g.a,g.b.]
  proof
   thus g. [.a,b.] = g.(a" * b" * a * b) by GROUP_5:19
                 .= g.(a" * b" * a) * g.b by Def7
                 .= g.(a" * b") * g.a * g.b by Def7
                 .= g.(a") * g.(b") * g.a * g.b by Def7
                 .= (g.a)" * g.(b") * g.a * g.b by Th41
                 .= (g.a)" * (g.b)" * g.a * g.b by Th41
                 .= [.g.a,g.b.] by GROUP_5:19;
  end;

theorem
   g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.]
  proof
   thus g. [.a1,a2,a3.] = g. [.[.a1,a2.],a3.] by GROUP_5:def 3
                      .= [.g. [.a1,a2.],g.a3.] by Th43
                      .= [.[.g.a1,g.a2.],g.a3.] by Th43
                      .= [.g.a1,g.a2,g.a3.] by GROUP_5:def 3;
  end;

theorem Th45:
 g.(a |^ n) = (g.a) |^ n
  proof
   defpred Q[Nat] means g.(a |^ $1) = (g.a) |^ $1;
A1: Q[0]
     proof
      thus g.(a |^ 0) = g.(1.G) by GROUP_1:43
                .= 1.H by Th40
                .= (g.a) |^ 0 by GROUP_1:43;
     end;
A2: for n st Q[n] holds Q[n + 1]
     proof
      let n;
      assume A3: Q[n];
      thus g.(a |^ (n + 1)) = g.(a |^ n * a) by GROUP_1:49
                      .= (g.a) |^ n * g.a by A3,Def7
                      .= (g.a) |^ (n + 1) by GROUP_1:49;
     end;
     for n holds Q[n] from Ind(A1,A2);
   hence thesis;
  end;

theorem
   g.(a |^ i) = (g.a) |^ i
  proof
     now per cases;
    suppose A1: i >= 0;
     hence g.(a |^ i) = g.(a |^ abs( i )) by GROUP_1:55
               .= (g.a) |^ abs( i ) by Th45
               .= (g.a) |^ i by A1,GROUP_1:55;
    suppose A2: i < 0;
     hence g.(a |^ i) = g.(a |^ abs( i ))" by GROUP_1:56
               .= (g.(a |^ abs( i )))" by Th41
               .= ((g.a) |^ abs( i ))" by Th45
               .= (g.a) |^ i by A2,GROUP_1:56;
   end;
   hence thesis;
  end;

theorem Th47:
 id the carrier of G is Homomorphism of G,G
  proof
   reconsider f = id the carrier of G
 as Function of the carrier of G, the carrier of G;
     now
    let a,b;
    thus f.(a * b) = a * b by FUNCT_1:35
                  .= f.a * b by FUNCT_1:35
                  .= f.a * f.b by FUNCT_1:35;
   end;
   hence thesis by Def7;
  end;

theorem Th48:
 h1 * h is Homomorphism of G,I
  proof
   reconsider f = h1 * h as
    Function of the carrier of G, the carrier of I;
     now
    let a,b;
    thus
       f.(a * b) = h1.(h.(a * b)) by FUNCT_2:21
              .= h1.(h.a * h.b) by Def7
              .= (h1.(h.a)) * (h1.(h.b)) by Def7
              .= f.a * (h1.(h.b)) by FUNCT_2:21
              .= f.a * f.b by FUNCT_2:21;
   end;
   hence thesis by Def7;
  end;

definition let G,H,I,h,h1;
 redefine func h1 * h -> Homomorphism of G,I;
 coherence by Th48;
end;

definition let G,H,g;
 redefine func rng g -> Subset of H;
 coherence by RELSET_1:12;
end;

definition let G,H;
 func 1:(G,H) -> Homomorphism of G,H means
  :Def8: for a holds it.a = 1.H;
 existence
  proof
   deffunc F(Element of G) = 1.H;
   consider f such that
A1: for a holds f.a = F(a) from LambdaD;
     f.(a * b) = f.a * f.b by A1,Lm1;
   then reconsider g = f as Homomorphism of G,H by Def7;
   take g;
   thus thesis by A1;
  end;
 uniqueness
  proof
   let g,h be Homomorphism of G,H such that
A2: for a holds g.a = 1.H and
A3: for a holds h.a = 1.H;
     for a holds g.a = h.a
    proof
     let a;
       g.a = 1.H & h.a = 1.H by A2,A3;
     hence thesis;
    end;
   hence thesis by FUNCT_2:113;
  end;
end;

theorem
   h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I)
  proof
    A1: now let a;
     thus (h1 * 1:(G,H)).a = h1.(1:(G,H).a) by FUNCT_2:21
                          .= h1.(1.H) by Def8
                          .= 1.I by Th40;
    end;
      now let a;
     thus (1:(H,I) * h).a = 1:(H,I).(h.a) by FUNCT_2:21
                          .= 1.I by Def8;
    end;
   hence thesis by A1,Def8;
  end;

definition let G; let N be normal Subgroup of G;
 func nat_hom N -> Homomorphism of G,G./.N means
  :Def9: for a holds it.a = a * N;
 existence
  proof
    defpred P[set,set] means ex a st $1 = a & $2 = a * N;
     A1: for x,y1,y2 st x in the carrier of G & P[x,y1] & P[x,y2] holds
             y1 = y2;
     A2: for x st x in the carrier of G ex y st P[x,y]
      proof let x;
        assume x in the carrier of G;
         then reconsider a = x as Element of G;
         reconsider y = a * N as set;
       take y;
       take a;
       thus thesis;
      end;
    consider f being Function such that A3: dom f = the carrier of G and
     A4: for x st x in the carrier of G holds P[x,f.x] from FuncEx(A1,A2);
       rng f c= the carrier of G./.N
      proof let x;
        assume x in rng f;
         then consider y such that A5: y in
 dom f and A6: f.y = x by FUNCT_1:def 5;
         consider a such that A7: y = a & f.y = a * N by A3,A4,A5;
            a * N = N * a by GROUP_3:140;
          then x in G./.N by A6,A7,Th28;
       hence thesis by RLVECT_1:def 1;
      end;
    then reconsider f as Function of the carrier of G, the carrier of G./.N
                                           by A3,FUNCT_2:def 1,RELSET_1:11
;
       now let a,b;
       consider a1 such that A8: a = a1 & f.a = a1 * N by A4;
       consider b1 such that A9: b = b1 & f.b = b1 * N by A4;
A10:       ex c being Element of G
             st c = a * b & f.(a * b) = c * N by A4;
        A11: @(f.a) = f.a & @(f.b) = f.b by Def6;
      thus f.a * f.b = @(f.a) * @(f.b) by Th24
                    .= (a1 * N) * b1 * N by A8,A9,A11,GROUP_3:10
                    .= a1 * (N * b1) * N by GROUP_2:128
                    .= a1 * (b1 * N) * N by GROUP_3:140
                    .= a1 * ((b1 * N) * N) by GROUP_3:9
                    .= a1 * (b1 * N) by Th6
                    .= f.(a * b) by A8,A9,A10,GROUP_2:127;
     end;
    then reconsider f as Homomorphism of G,G./.N by Def7;
   take f;
   let a;
      ex b st a = b & f.a = b * N by A4;
   hence thesis;
  end;
 uniqueness
  proof let n1,n2 be Homomorphism of G,G./.N such that
    A12: for a holds n1.a = a * N and
    A13: for a holds n2.a = a * N;
      now let a;
        n1.a = a * N & n2.a = a * N by A12,A13;
     hence n1.a = n2.a;
    end;
   hence thesis by FUNCT_2:113;
  end;
end;

definition let G,H,g;
 func Ker g -> strict Subgroup of G means
  :Def10: the carrier of it = {a : g.a = 1.H};
 existence
  proof
    defpred P[set] means g.$1 = 1.H;
    reconsider A = {a : P[a]} as Subset of G from SubsetD;
       g.(1.G) = 1.H by Th40;
     then A1: 1.G in A;
     A2: now let a,b;
       assume that A3: a in A and A4: b in A;
A5:        ex a1 st a1 = a & g.a1 = 1.H by A3;
A6:        ex b1 st b1 = b & g.b1 = 1.H by A4;
           g.(a * b) = g.a * g.b by Def7
                  .= 1.H by A5,A6,GROUP_1:def 4;
      hence a * b in A;
     end;
       now let a;
       assume a in A;
        then ex a1 st a1 = a & g.a1 = 1.H;
         then g.(a") = (1.H)" by Th41
               .= 1.H by GROUP_1:16;
      hence a" in A;
     end;
    then consider B being strict Subgroup of G such that
    A7: the carrier of B = A by A1,A2,GROUP_2:61;
    reconsider B as strict Subgroup of G;
   take B;
   thus thesis by A7;
  end;
 uniqueness by GROUP_2:68;
end;

definition let G,H,g;
 cluster Ker g -> normal;
 coherence
  proof
    defpred P[set] means g.$1 = 1.H;
    reconsider A = {a : P[a]} as Subset of G from SubsetD;
       g.(1.G) = 1.H by Th40;
     then A1: 1.G in A;
     A2: now let a,b;
       assume that A3: a in A and A4: b in A;
A5:        ex a1 st a1 = a & g.a1 = 1.H by A3;
A6:        ex b1 st b1 = b & g.b1 = 1.H by A4;
           g.(a * b) = g.a * g.b by Def7
                  .= 1.H by A5,A6,GROUP_1:def 4;
      hence a * b in A;
     end;
       now let a;
       assume a in A;
        then ex a1 st a1 = a & g.a1 = 1.H;
         then g.(a") = (1.H)" by Th41
               .= 1.H by GROUP_1:16;
      hence a" in A;
     end;
    then consider B being strict Subgroup of G such that
    A7: the carrier of B = A by A1,A2,GROUP_2:61;
       now let a;
         now let b;
         assume b in B |^ a;
          then consider c being Element of G such that
           A8: b = c |^ a and A9: c in B by GROUP_3:70;
             c in A by A7,A9,RLVECT_1:def 1;
          then ex a1 st c = a1 & g.a1 = 1.H;
           then g.b = (1.H) |^ (g.a) by A8,Th42
              .= 1.H by GROUP_3:22;
           then b in A;
        hence b in B by A7,RLVECT_1:def 1;
       end;
      hence B |^ a is Subgroup of B by GROUP_2:67;
     end;
    then B is normal Subgroup of G by GROUP_3:145;
   hence thesis by A7,Def10;
  end;
end;

theorem Th50:
 a in Ker h iff h.a = 1.H
  proof
   thus a in Ker h implies h.a = 1.H
    proof
     assume a in Ker h;
      then a in the carrier of Ker h by RLVECT_1:def 1;
      then a in {b : h.b = 1.H} by Def10;
      then ex b st a = b & h.b = 1.H;
     hence thesis;
    end;
    assume h.a = 1.H;
     then a in {b : h.b = 1.H};
     then a in the carrier of Ker h by Def10;
   hence thesis by RLVECT_1:def 1;
  end;

theorem
   for G,H being strict Group holds
 Ker 1:(G,H) = G
  proof let G,H be strict Group;
      now let a be Element of G;
        1:(G,H).a = 1.H by Def8;
     hence a in Ker 1:(G,H) by Th50;
    end;
   hence thesis by GROUP_2:71;
  end;

theorem Th52:
 for N being strict normal Subgroup of G holds
 Ker nat_hom N = N
  proof let N be strict normal Subgroup of G;
   let a;
   thus a in Ker nat_hom N implies a in N
    proof assume a in Ker nat_hom N;
      then (nat_hom N).a = 1.(G./.N) & (nat_hom N).a = a * N &
           1.(G./.N) = carr N by Def9,Th29,Th50;
     hence a in N by GROUP_2:136;
    end;
    assume a in N;
     then a * N = carr N & (nat_hom N).a = a * N &
          1.(G./.N) = carr N by Def9,Th29,GROUP_2:136;
   hence thesis by Th50;
  end;

definition let G,H,g;
 func Image g -> strict Subgroup of H means
  :Def11: the carrier of it = g .: (the carrier of G);
 existence
  proof
      the carrier of G c= the carrier of G;
    then reconsider X = the carrier of G as Subset of G;
    set S = g .: X;
A1:   dom g = the carrier of G & X /\ X = X & X <> {} by FUNCT_2:def 1;
     then X meets X by XBOOLE_0:def 7;
     then A2: S <> {} by A1,RELAT_1:151;
     A3: now let c,d;
       assume that A4: c in S and A5: d in S;
        consider a such that a in X and A6: c = g.a by A4,FUNCT_2:116;
        consider b such that b in X and A7: d = g.b by A5,FUNCT_2:116;
           c * d = g.(a * b) & a * b in the carrier of G by A6,A7,Def7;
      hence c * d in S by FUNCT_2:43;
     end;
       now let c;
       assume c in S;
        then consider a such that a in X and A8: c = g.a by FUNCT_2:116;
           a" in the carrier of G & g.(a") = c" by A8,Th41;
      hence c" in S by FUNCT_2:43;
     end;
    then consider D being strict Subgroup of H such that
    A9: the carrier of D = S by A2,A3,GROUP_2:61;
   take D;
   thus thesis by A9;
  end;
 uniqueness by GROUP_2:68;
end;

theorem Th53:
 rng g = the carrier of Image g
  proof
     the carrier of Image g = g .: (the carrier of G) by Def11
                         .= g .: (dom g) by FUNCT_2:def 1
                         .= rng g by RELAT_1:146;
   hence thesis;
  end;

theorem Th54:
 x in Image g iff ex a st x = g.a
  proof
   thus x in Image g implies ex a st x = g.a
    proof assume x in Image g;
       then x in the carrier of Image g by RLVECT_1:def 1;
       then x in g .: (the carrier of G) by Def11;
      then consider y such that y in dom g and A1: y in the carrier of G and
       A2: g.y = x by FUNCT_1:def 12;
      reconsider y as Element of G by A1;
     take y;
     thus thesis by A2;
    end;
    given a such that A3: x = g.a;
       a in the carrier of G & the carrier of G = dom g by FUNCT_2:def 1;
     then x in g .: (the carrier of G) by A3,FUNCT_1:def 12;
     then x in the carrier of Image g by Def11;
   hence thesis by RLVECT_1:def 1;
  end;

theorem
   Image g = gr rng g
  proof
       rng g = the carrier of Image g & the carrier of Image g = carr Image g
                                                           by Th53,GROUP_2:def
9;
   hence thesis by GROUP_4:40;
  end;

theorem
   Image 1:(G,H) = (1).H
  proof set g = 1:(G,H);
      1.H in Image g by GROUP_2:55;
    then 1.H in the carrier of Image g by RLVECT_1:def 1;
    then A1: {1.H} c= the carrier of Image g by ZFMISC_1:37;
      the carrier of Image g c= {1.H}
     proof let x;
       assume x in the carrier of Image g;
         then x in g .: (the carrier of G) by Def11;
        then consider y such that y in dom g and A2: y in the carrier of G and
         A3: g.y = x by FUNCT_1:def 12;
        reconsider y as Element of G by A2;
           g.y = 1.H by Def8;
      hence thesis by A3,TARSKI:def 1;
     end;
    then the carrier of Image g = {1.H} by A1,XBOOLE_0:def 10;
   hence thesis by GROUP_2:def 7;
  end;

theorem Th57:
 for N being normal Subgroup of G holds
 Image nat_hom N = G./.N
  proof let N be normal Subgroup of G;
      now let S be Element of G./.N;
      consider a such that A1: S = a * N & S = N * a by Th26;
         (nat_hom N).a = a * N by Def9;
     hence S in Image nat_hom N by A1,Th54;
    end;
   hence thesis by GROUP_2:71;
  end;

theorem Th58:
 h is Homomorphism of G,Image h
  proof
     h is Function of the carrier of G, the carrier of Image h
    proof
A1:     rng h = the carrier of Image h by Th53;
       dom h = the carrier of G by FUNCT_2:def 1;
     hence thesis by A1,FUNCT_2:def 1,RELSET_1:11;
    end;
   then reconsider f' = h as
         Function of the carrier of G, the carrier of Image h;
     now
    let a,b;
    thus f'.a * f'.b = h.a * h.b by GROUP_2:52
                    .= f'.(a * b) by Def7;
   end;
   hence thesis by Def7;
  end;

theorem Th59:
 G is finite implies Image g is finite
  proof
   assume G is finite;
   then the carrier of G is finite by GROUP_1:def 13;
   then g .: (the carrier of G) is finite by FINSET_1:17;
   then the carrier of Image g is finite by Def11;
   hence thesis by GROUP_1:def 13;
  end;

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

theorem
   G is commutative Group implies Image g is commutative
  proof assume A1: G is commutative Group;
   let h1,h2 be Element of Image g;
    reconsider c = h1, d = h2 as Element of H by GROUP_2:51;
       h1 in Image g by RLVECT_1:def 1;
    then consider a such that A2: h1 = g.a by Th54;
       h2 in Image g by RLVECT_1:def 1;
    then consider b such that A3: h2 = g.b by Th54;
   thus h1 * h2 = c * d by GROUP_2:52
               .= g.(a * b) by A2,A3,Def7
               .= g.(b * a) by A1,Lm2
               .= d * c by A2,A3,Def7
               .= h2 * h1 by GROUP_2:52;
  end;

theorem Th61:
 Ord Image g <=` Ord G
  proof
A1: Card (g .: (the carrier of G)) <=` Card (the carrier of G) by CARD_2:3;
     Ord Image g = Card (the carrier of Image g) by GROUP_1:def 12
              .= Card (g .: (the carrier of G)) by Def11;
   hence thesis by A1,GROUP_1:def 12;
  end;

theorem
   G is finite implies ord Image g <= ord G
  proof
   assume A1: G is finite;
   then A2: Image g is finite by Th59;
    consider c being finite set such that
A3:  c = the carrier of G & ord G = card c by A1,GROUP_1:def 14;
    consider ci being finite set such that
A4:  ci = the carrier of Image g & ord Image g = card ci by A2,GROUP_1:def 14;
     Ord Image g <=` Ord G by Th61;
   then Card (the carrier of Image g) <=` Ord G by GROUP_1:def 12;
   then Card (the carrier of Image g) <=`
 Card (the carrier of G) by GROUP_1:def 12;
   hence thesis by A3,A4,CARD_2:57;
  end;

definition
 let G,H,h;
 attr h is being_monomorphism means :Def12: h is one-to-one;
  synonym h is_monomorphism;
 attr h is being_epimorphism means :Def13: rng h = the carrier of H;
  synonym h is_epimorphism;
end;

theorem
   h is_monomorphism & c in Image h implies h.(h".c) = c
  proof
   assume that A1: h is_monomorphism and
               A2: c in Image h;
   reconsider h' = h as
          Function of the carrier of G,the carrier of Image h by Th58;
A3: h' is one-to-one by A1,Def12;
     h'.(h'".c) = c
    proof
A4:   rng h' = the carrier of Image h by Th53;
       c in the carrier of Image h by A2,RLVECT_1:def 1;
     hence thesis by A3,A4,FUNCT_1:57;
    end;
   hence thesis;
  end;

theorem Th64:
 h is_monomorphism implies h".(h.a) = a
  proof
   assume h is one-to-one;
   hence thesis by FUNCT_2:32;
  end;

theorem Th65:
 h is_monomorphism implies h" is Homomorphism of Image h,G
  proof
   assume A1: h is one-to-one;
    then A2: h is_monomorphism by Def12;
   reconsider Imh = Image h as Group;
      h" is Function of the carrier of Imh,the carrier of G
     proof
      A3: h is Function of the carrier of G,the carrier of Imh by Th58;
    rng h = the carrier of Imh by Th53;
      hence thesis by A1,A3,FUNCT_2:31;
     end;
   then reconsider h' = h" as Function of the carrier of Imh,
                                      the carrier of G;
     now
    let a,b be Element of Imh;
    reconsider a' = a as Element of H by GROUP_2:51;
    reconsider b' = b as Element of H by GROUP_2:51;
A4:   a' in Imh & b' in Imh by RLVECT_1:def 1;
    then consider a1 being Element of G such that
    A5: h.a1 = a' by Th54;
    consider b1 being Element of G such that
    A6: h.b1 = b' by A4,Th54;
    thus h'.(a * b) = h'.(h.a1 * h.b1) by A5,A6,GROUP_2:52
                   .= h'.(h.(a1 * b1)) by Def7
                   .= a1 * b1 by A2,Th64
                   .= h'.a * b1 by A2,A5,Th64
                   .= h'.a * h'.b by A2,A6,Th64;
   end;
   hence thesis by Def7;
  end;

theorem Th66:
 h is_monomorphism iff Ker h = (1).G
  proof
   thus h is_monomorphism implies Ker h = (1).G
    proof
     assume A1: h is one-to-one;
       now
      let x;
      thus x in the carrier of Ker h iff x = 1.G
       proof
        thus x in the carrier of Ker h implies x = 1.G
         proof
          assume A2: x in the carrier of Ker h;
          then x in Ker h by RLVECT_1:def 1;
          then x in G by GROUP_2:49;
          then reconsider a = x as Element of G
            by RLVECT_1:def 1;
            a in Ker h by A2,RLVECT_1:def 1;
          then h.a = 1.H by Th50
                  .= h.(1.G) by Th40;
          hence thesis by A1,Th1;
         end;
        assume A3: x = 1.G;
        then reconsider a = x as Element of G;
          h.a = 1.H by A3,Th40;
        then a in Ker h by Th50;
        hence thesis by RLVECT_1:def 1;
       end;
     end;
     then the carrier of Ker h = {1.G} by TARSKI:def 1;
     hence thesis by GROUP_2:def 7;
    end;
   assume Ker h = (1).G;
   then A4: the carrier of Ker h = {1.G} by GROUP_2:def 7;
     now
    let a,b;
    assume that
     A5: a <> b and
     A6: h.a = h.b;
   h.a * h.(a") = h.(a * a") by Def7
                .= h.(1.G) by GROUP_1:def 5
                .= 1.H by Th40;
    then 1.H = h.(b * a") by A6,Def7;
    then b * a" in Ker h by Th50;
    then A7: b * a" in the carrier of Ker h by RLVECT_1:def 1;
      a = 1.G * a by GROUP_1:def 4
     .= b * a" * a by A4,A7,TARSKI:def 1
     .= b * (a" * a) by VECTSP_1:def 16
     .= b * 1.G by GROUP_1:def 5
     .= b by GROUP_1:def 4;
    hence contradiction by A5;
   end;
  then for a,b st h.a = h.b holds a = b;
  then h is one-to-one by Th1;
  hence thesis by Def12;
 end;

theorem Th67:
 for H being strict Group, h being Homomorphism of G,H holds
 h is_epimorphism iff Image h = H
  proof let H be strict Group, h be Homomorphism of G,H;
   thus h is_epimorphism implies Image h = H
    proof assume rng h = the carrier of H;
      then the carrier of Image h = the carrier of H by Th53;
     hence thesis by GROUP_2:70;
    end;
    assume A1: Image h = H;
       the carrier of H c= rng h
      proof let x;
        assume x in the carrier of H;
          then x in h .: (the carrier of G) by A1,Def11;
         then ex y st y in dom h & y in the carrier of G &
 h.y = x by FUNCT_1:def 12;
       hence thesis by FUNCT_1:def 5;
      end;
     then rng h = the carrier of H by XBOOLE_0:def 10;
   hence thesis by Def13;
  end;

theorem Th68:
 for H being strict Group, h being Homomorphism of G,H holds
 h is_epimorphism implies
  for c being Element of H ex a st h.a = c
   proof let H be strict Group, h be Homomorphism of G,H;
    assume h is_epimorphism;
    then A1: Image h = H by Th67;
      now
     let c be Element of H;
       c in Image h by A1,RLVECT_1:def 1;
     hence ex a st h.a = c by Th54;
    end;
    hence thesis;
   end;

theorem Th69:
 for N being normal Subgroup of G holds
 nat_hom N is_epimorphism
  proof let N be normal Subgroup of G;
      Image nat_hom N = G./.N by Th57;
   hence thesis by Th67;
  end;

definition
 let G,H,h;
 attr h is being_isomorphism
 means :Def14: h is_epimorphism & h is_monomorphism;
  synonym h is_isomorphism;
end;

theorem Th70:
 h is_isomorphism iff rng h = the carrier of H & h is one-to-one
  proof
   thus h is_isomorphism implies
     rng h = the carrier of H & h is one-to-one
    proof
     assume h is_epimorphism & h is_monomorphism;
     hence thesis by Def12,Def13;
    end;
   assume rng h = the carrier of H & h is one-to-one;
   hence h is_epimorphism & h is_monomorphism by Def12,Def13;
  end;

theorem
   h is_isomorphism implies dom h = the carrier of G & rng h = the carrier of H
  proof
   assume h is_isomorphism;
   then h is_epimorphism by Def14;
   hence thesis by Def13,FUNCT_2:def 1;
  end;

theorem Th72:
 for H being strict Group, h being Homomorphism of G,H holds
 h is_isomorphism implies h" is Homomorphism of H,G
  proof let H be strict Group, h be Homomorphism of G,H;
   assume A1: h is_epimorphism & h is_monomorphism;
   then H = Image h by Th67;
   hence thesis by A1,Th65;
  end;

theorem Th73:
 h is_isomorphism & g1 = h" implies g1 is_isomorphism
  proof
   assume that A1:  h is_isomorphism and
               A2:  g1 = h";
A3: h is one-to-one by A1,Th70;
   then A4: g1 is one-to-one by A2,FUNCT_1:62;
A5: dom h = the carrier of G by FUNCT_2:def 1;
      rng g1 = dom h by A2,A3,FUNCT_1:55;
   hence thesis by A4,A5,Th70;
  end;

theorem Th74:
 h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism
  proof
   assume A1: h is_isomorphism & h1 is_isomorphism;
then A2: h is one-to-one & h1 is one-to-one by Th70;
A3: rng(h1 * h) = the carrier of I
     proof
A4:  dom h1 = the carrier of H by FUNCT_2:def 1;
    rng h = the carrier of H by A1,Th70;
      hence rng(h1 * h) = rng h1 by A4,RELAT_1:47
                       .= the carrier of I by A1,Th70;
     end;
   h1 * h is one-to-one by A2,FUNCT_1:46;
   hence thesis by A3,Th70;
  end;

theorem Th75:
 for G being Group holds
 nat_hom (1).G is_isomorphism
  proof let G be Group;
    set g = nat_hom (1).G;
      Ker g = (1).G by Th52;
    then g is_monomorphism & g is_epimorphism by Th66,Th69;
   hence nat_hom (1).G is_isomorphism by Def14;
  end;

definition
 let G,H;
 pred G,H are_isomorphic means :Def15: ex h st h is_isomorphism;
 reflexivity
  proof let G;
   reconsider i = id the carrier of G as Homomorphism of G,G by Th47;
     i is one-to-one & rng i = the carrier of G by FUNCT_2:def 3;
   then i is_isomorphism by Th70;
   hence thesis;
  end;
end;

canceled;

theorem Th77:
 for G,H being strict Group holds
 G,H are_isomorphic implies H,G are_isomorphic
  proof let G,H be strict Group;
   assume G,H are_isomorphic;
   then consider h being Homomorphism of G,H such that
   A1: h is_isomorphism by Def15;
    reconsider g = h" as Homomorphism of H,G by A1,Th72;
   take g;
   thus thesis by A1,Th73;
  end;

theorem
   G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic
  proof
   assume that
A1: G,H are_isomorphic and
A2: H,I are_isomorphic;
   consider g such that A3:  g is_isomorphism by A1,Def15;
   consider h1 such that A4: h1 is_isomorphism by A2,Def15;
     (h1 * g) is_isomorphism by A3,A4,Th74;
   hence thesis by Def15;
  end;

theorem
   h is_monomorphism implies G,Image h are_isomorphic
  proof
   assume A1: h is one-to-one;
   reconsider ih = h as Homomorphism of G,Image h by Th58;
   take ih;
A2: ih is_monomorphism by A1,Def12;
      now
       the carrier of Image h = rng ih by Th53;
     hence ih is_epimorphism by Def13;
    end;
   hence thesis by A2,Def14;
  end;

theorem Th80:
 for G,H being strict Group holds
 G is trivial & H is trivial implies G,H are_isomorphic
  proof let G,H be strict Group;
   assume G is trivial & H is trivial;
   then A1: G = (1).G & H = (1).H by Th13;
   take 1:(G,H);
   set h = 1:(G,H);
A2: h is_epimorphism
    proof
       the carrier of (1).G = {1.G} by GROUP_2:def 7;
     then rng h = {h.(1.G)} by A1,FUNCT_2:62
               .= {1.H} by Def8
               .= the carrier of (1).H by GROUP_2:def 7;
     hence thesis by A1,Def13;
    end;
     h is_monomorphism
    proof
       now
      let a,b be Element of G;
      assume h.a = h.b;
        a in the carrier of (1).G & b in the carrier of (1).G by A1;
      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;
     end;
     then h is one-to-one by Th1;
     hence thesis by Def12;
    end;
   hence thesis by A2,Def14;
  end;

theorem
   (1).G,(1).H are_isomorphic
  proof
     (1).G is trivial & (1).H is trivial by Th11;
   hence thesis by Th80;
  end;

theorem
   for G being strict Group holds
 G,G./.(1).G are_isomorphic & G./.(1).G,G are_isomorphic
  proof let G be strict Group;
      nat_hom (1).G is_isomorphism by Th75;
   hence G,G./.(1).G are_isomorphic by Def15;
   hence thesis by Th77;
  end;

theorem
   for G being Group holds
 G./.(Omega).G is trivial
  proof let G be Group;
     the carrier of G./.(Omega).G = Cosets (Omega).G by Th22
                                   .= Left_Cosets (Omega).G by Def3
                                   .= {the carrier of G} by GROUP_2:172;
   hence thesis by Def2;
  end;

theorem Th84:
 for G,H being strict Group, h being Homomorphism of G,H holds
 G,H are_isomorphic implies Ord G = Ord H
  proof let G,H be strict Group, h be Homomorphism of G,H;
   assume A1: G,H are_isomorphic;
   then consider h being Homomorphism of G,H such that
   A2:  h is_isomorphism by Def15;
     H,G are_isomorphic by A1,Th77;
   then consider g1 being Homomorphism of H,G such that
   A3: g1 is_isomorphism by Def15;
     h is_epimorphism by A2,Def14;
    then Image h = H by Th67;
    then A4: Ord H <=` Ord G by Th61;
     g1 is_epimorphism by A3,Def14;
    then Image g1 = G by Th67;
    then Ord G <=` Ord H by Th61;
   hence thesis by A4,XBOOLE_0:def 10;
  end;

Lm3:
 G,H are_isomorphic & G is finite implies H is finite
  proof
   assume that A1: G,H are_isomorphic and
               A2: G is finite;
   consider h such that A3: h is_isomorphism by A1,Def15;
     h is_epimorphism by A3,Def14;
   then A4: rng h = the carrier of H by Def13;
 the carrier of G is finite by A2,GROUP_1:def 13;
   then dom h is finite by FUNCT_2:def 1;
   then the carrier of H is finite by A4,FINSET_1:26;
   hence thesis by GROUP_1:def 13;
  end;

Lm4:
 for G,H being strict Group holds
 G,H are_isomorphic & H is finite implies G is finite
  proof let G,H be strict Group;
   assume that A1: G,H are_isomorphic and
               A2: H is finite;
     H,G are_isomorphic by A1,Th77;
   hence thesis by A2,Lm3;
  end;

theorem
  for G,H being strict Group holds
 G,H are_isomorphic & (G is finite or H is finite) implies
  (G is finite & H is finite) by Lm3,Lm4;

theorem Th86:
 for G,H being strict Group holds
 G,H are_isomorphic & (G is finite or H is finite) implies ord G = ord H
  proof let G,H be strict Group;
   assume that A1: G,H are_isomorphic and
               A2: G is finite or H is finite;
     Ord G = Ord H by A1,Th84;
   then A3: Card (the carrier of G) = Ord H by GROUP_1:def 12
                                   .= Card (the carrier of H) by GROUP_1:def 12
;
A4: H is finite & G is finite by A1,A2,Lm3,Lm4;
    then consider cH being finite set such that
A5: cH = the carrier of H & ord H = card cH by GROUP_1:def 14;
    consider cG being finite set such that
A6: cG = the carrier of G & ord G = card cG by A4,GROUP_1:def 14;
   thus thesis by A3,A5,A6;
  end;

theorem
   for G,H being strict Group holds
 G,H are_isomorphic & G is trivial implies H is trivial
  proof let G,H be strict Group;
   assume that A1: G,H are_isomorphic and
               A2: G is trivial;
A3: ord G = 1 & G is finite by A2,Th12;
   then A4: ord H = 1 by A1,Th86;
     H is finite by A1,A3,Lm3;
   hence thesis by A4,Th12;
  end;

Lm5:
 for G,H being strict Group holds
 G,H are_isomorphic & G is trivial implies H is trivial
  proof let G,H be strict Group;
   assume that A1: G,H are_isomorphic and
               A2: G is trivial;
A3: ord G = 1 & G is finite by A2,Th12;
   then A4: ord H = 1 by A1,Th86;
     H is finite by A1,A3,Lm3;
   hence thesis by A4,Th12;
  end;

Lm6:
 for G,H being strict Group holds
 G,H are_isomorphic & H is trivial implies G is trivial
  proof let G,H be strict Group;
   assume that A1: G,H are_isomorphic and
               A2: H is trivial;
     H,G are_isomorphic by A1,Th77;
   hence thesis by A2,Lm5;
  end;

theorem
   for G,H being strict Group holds
 G,H are_isomorphic & (G is trivial or H is trivial) implies
  G is trivial & H is trivial by Lm5,Lm6;

Lm7:
 for H being strict Group, h being Homomorphism of G,H holds
 G,H are_isomorphic & G is commutative Group implies H is commutative Group
  proof let H be strict Group, h be Homomorphism of G,H;
   assume that A1: G,H are_isomorphic and
               A2: G is commutative Group;
   consider h being Homomorphism of G,H such that
   A3: h is_isomorphism by A1,Def15;
A4: h is_epimorphism by A3,Def14;
     now
    let c,d be Element of H;
    consider a such that A5: h.a = c by A4,Th68;
    consider b such that A6: h.b = d by A4,Th68;
    thus c * d = h.(a * b) by A5,A6,Def7
              .= h.(b * a) by A2,Lm2
              .= d * c by A5,A6,Def7;
   end;
   hence thesis by VECTSP_1:def 17;
  end;

Lm8:
 for G,H being strict Group, h being Homomorphism of G,H holds
 G,H are_isomorphic & H is commutative Group implies G is commutative Group
  proof let G,H be strict Group, h be Homomorphism of G,H;
   assume that A1: G,H are_isomorphic and
               A2: H is commutative Group;
     H,G are_isomorphic by A1,Th77;
   hence thesis by A2,Lm7;
  end;

theorem
   for G,H being strict Group, h being Homomorphism of G,H holds
 G,H are_isomorphic & (G is commutative Group or H is commutative Group)
  implies (G is commutative Group & H is commutative Group) by Lm7,Lm8;

Lm9:
 G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic &
  ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
   g = h * nat_hom Ker g
  proof set I = G./.Ker g; set J = Image g;
    defpred P[set,set] means for a st $1 = a * Ker g holds $2 = g.a;
     A1: for S being Element of I
     ex T being Element of J st P[S,T]
           proof let S be Element of I;
             consider a such that A2: S = a * Ker g & S = Ker g * a by Th26;
                g.a in J by Th54;
             then reconsider T = g.a as Element of J
               by RLVECT_1:def 1;
            take T;
            let b;
             assume S = b * Ker g;
              then a" * b in Ker g by A2,GROUP_2:137;
              then 1.H = g.(a" * b) by Th50
                      .= g.(a") * g.b by Def7
                      .= (g.a)" * g.b by Th41;
              then g.b = (g.a)"" by GROUP_1:20;
            hence thesis by GROUP_1:19;
           end;
    consider f being Function of the carrier of I,the carrier of J such that
     A3: for S being Element of I holds P[S,f.S]
       from FuncExD(A1);
       now let S,T be Element of G./.Ker g;
       consider a such that A4: S = a * Ker g and S = Ker g * a by Th26;
       consider b such that A5: T = b * Ker g and A6: T = Ker g * b by Th26;
          f.S = g.a & f.T = g.b by A3,A4,A5;
        then A7: f.S * f.T = g.a * g.b by GROUP_2:52
                         .= g.(a * b) by Def7;
           @S = S & @T = T by Def6;
        then S * T = (a * Ker g) * (Ker g * b) by A4,A6,Th24
             .= (a * Ker g) * Ker g * b by GROUP_3:12
             .= a * Ker g * b by Th6
             .= a * (Ker g * b) by GROUP_2:128
             .= a * (b * Ker g) by GROUP_3:140
             .= a * b * Ker g by GROUP_2:127;
      hence f.(S * T) = f.S * f.T by A3,A7;
     end;
    then reconsider f as Homomorphism of G./.Ker g,J by Def7;
       the carrier of J c= rng f
      proof let x;
        assume x in the carrier of J;
          then x in Image g by RLVECT_1:def 1;
         then consider a such that A8: x = g.a by Th54;
         reconsider S = a * Ker g as Element of I by Th27;
            f.S = g.a & S in the carrier of I & the carrier of I = dom f
           by A3,FUNCT_2:def 1;
       hence thesis by A8,FUNCT_1:def 5;
      end;
     then A9: rng f = the carrier of J by XBOOLE_0:def 10;
A10:     f is one-to-one
      proof let y1,y2;
        assume y1 in dom f & y2 in dom f;
         then reconsider S = y1, T = y2 as Element of I
           by FUNCT_2:def 1;
         consider a such that A11: S = a * Ker g and S = Ker g * a by Th26;
         consider b such that A12: T = b * Ker g and T = Ker g * b by Th26;
        assume A13: f.y1 = f.y2;
            f.S = g.a & f.T = g.b by A3,A11,A12;
          then (g.b)" * g.a = 1.H by A13,GROUP_1:def 5;
          then 1.H = g.(b") * g.a by Th41
                  .= g.(b" * a) by Def7;
          then b" * a in Ker g by Th50;
       hence thesis by A11,A12,GROUP_2:137;
      end;
     then f is_isomorphism by A9,Th70;
   hence G./.Ker g,Image g are_isomorphic by Def15;
   hence Image g,G./.Ker g are_isomorphic by Th77;
   take f;
     A14: dom nat_hom Ker g = the carrier of G & dom g = the carrier of G
                                                                 by FUNCT_2:def
1;
   thus f is_isomorphism by A9,A10,Th70;
     A15: now let x;
       thus x in dom g implies x in dom nat_hom Ker g & (nat_hom Ker g).x in
 dom f
        proof assume A16: x in dom g;
         hence x in dom nat_hom Ker g by A14;
            (nat_hom Ker g).x in rng nat_hom Ker g &
               rng nat_hom Ker g c= the carrier of I &
               dom f = the carrier of I by A14,A16,FUNCT_1:def 5,FUNCT_2:def 1;
         hence (nat_hom Ker g).x in dom f;
        end;
        assume that A17: x in dom nat_hom Ker g and (nat_hom Ker g).x in dom f
;
      thus x in dom g by A14,A17;
     end;
       now let x;
       assume x in dom g;
        then reconsider a = x as Element of G by FUNCT_2:def 1
;
            (nat_hom Ker g).a = a * Ker g by Def9;
      hence g.x = f.((nat_hom Ker g).x) by A3;
     end;
   hence thesis by A15,FUNCT_1:20;
  end;

theorem
   G./.Ker g,Image g are_isomorphic & Image g, G./.Ker g are_isomorphic by Lm9;

theorem
   ex h being Homomorphism of G./.Ker g,Image g st h is_isomorphism &
  g = h * nat_hom Ker g by Lm9;

theorem
   for M being strict normal Subgroup of G
 for J being strict normal Subgroup of G./.M st
  J = N./.(N,M)`*` & M is Subgroup of N holds (G./.M)./.J,G./.N are_isomorphic
   proof let M be strict normal Subgroup of G;
    let J be strict normal Subgroup of G./.M;
     assume that A1: J = N./.(N,M)`*` and A2: M is Subgroup of N;
      defpred P[set,set] means for a st $1 = a * M holds $2 = a * N;
       A3: for x being Element of G./.M
         ex y being Element of G./.N st
             P[x,y]
        proof let x be Element of G./.M;
          consider a such that A4: x = a * M and x = M * a by Th26;
          reconsider y = a * N as Element of G./.N by Th27;
         take y;
         let b;
          assume x = b * M;
           then a" * b in M by A4,GROUP_2:137;
           then a" * b in N by A2,GROUP_2:49;
         hence thesis by GROUP_2:137;
        end;
      consider f being Function of the carrier of G./.M, the carrier of G./.N
       such that A5: for x being Element of G./.M holds P[x,f.x]
                                               from FuncExD(A3);
         now let x,y be Element of G./.M;
         consider a such that A6: x = a * M and x = M * a by Th26;
         consider b such that A7: y = b * M and y = M * b by Th26;
          A8: f.x = @(f.x) & f.y = @(f.y) by Def6;
          A9: f.x = a * N & f.y = b * N by A5,A6,A7;
          A10: f.x * f.y = @(f.x) * @(f.y) by Th24
                      .= a * N * b * N by A8,A9,GROUP_3:10
                      .= a * (N * b) * N by GROUP_2:128
                      .= a * (b * N) * N by GROUP_3:140
                      .= a * ((b * N) * N) by GROUP_3:9
                      .= a * (b * N) by Th6
                      .= a * b * N by GROUP_2:127;
          A11: @x = x & @y = y by Def6;
            x * y = @x * @y by Th24
               .= a * M * b * M by A6,A7,A11,GROUP_3:10
               .= a * (M * b) * M by GROUP_2:128
               .= a * (b * M) * M by GROUP_3:140
               .= a * ((b * M) * M) by GROUP_3:9
               .= a * (b * M) by Th6
               .= a * b * M by GROUP_2:127;
        hence f.(x * y) = f.x * f.y by A5,A10;
       end;
      then reconsider f as Homomorphism of G./.M,G./.N by Def7;
       A12: Ker f = J
        proof let S be Element of G./.M;
         thus S in Ker f implies S in J
          proof assume S in Ker f;
             then A13: f.S = 1.(G./.N) by Th50
                        .= carr N by Th29;
            consider a such that A14: S = a * M & S = M * a by Th26;
               f.S = a * N by A5,A14;
             then a in N by A13,GROUP_2:136;
            then reconsider q = a as Element of N
              by RLVECT_1:def 1;
               (N,M)`*` = M by A2,Def1;
             then S = q * (N,M)`*` & S = (N,M)`*` * q by A14,Th2;
           hence thesis by A1,Th28;
          end;
          assume S in J;
           then consider a being Element of N such that
            A15: S = a * (N,M)`*` & S = (N,M)`*` * a by A1,Th28;
           reconsider a' = a as Element of G by GROUP_2:51;
              (N,M)`*` = M by A2,Def1;
            then S = a' * M by A15,Th2;
            then f.S = a' * N & a in N by A5,RLVECT_1:def 1;
            then f.S = carr N by GROUP_2:136
                    .= 1.(G./.N) by Th29;
         hence thesis by Th50;
        end;
         the carrier of G./.N c= rng f
        proof let x;
          assume x in the carrier of G./.N;
            then x in G./.N by RLVECT_1:def 1;
           then consider a such that A16: x = a * N & x = N * a by Th28;
           reconsider S = a * M as Element of G./.M by Th27;
              f.S = a * N & S in
 the carrier of G./.M & dom f = the carrier of G./.M
                                                                     by A5,
FUNCT_2:def 1;
         hence thesis by A16,FUNCT_1:def 5;
        end;
       then rng f = the carrier of G./.N by XBOOLE_0:def 10;
       then f is_epimorphism by Def13;
       then Image f = G./.N by Th67;
    hence thesis by A12,Lm9;
   end;

theorem
   for N being strict normal Subgroup of G holds
 (B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic
  proof let N be strict normal Subgroup of G;
        set f = nat_hom N; set g = f | (the carrier of B);
        set I = (B "\/" N)./.(B "\/" N,N)`*`; set J = (B "\/" N,N)`*`;
     A1: B is Subgroup of B "\/" N by GROUP_4:78;
      A2: dom g = dom f /\ (the carrier of B) & dom f = the carrier of G &
          the carrier of B c= the carrier of G by FUNCT_2:def 1,GROUP_2:def 5,
RELAT_1:90;
     then A3: dom g = the carrier of B by XBOOLE_1:28;
A4:     N is Subgroup of B "\/" N by GROUP_4:78;
     then A5: N = (B "\/" N,N)`*` by Def1;
     A6: I is Subgroup of G./.N by A4,Th34;
        rng g c= the carrier of I
      proof let y;
        assume y in rng g;
         then consider x such that A7: x in
 dom g and A8: g.x = y by FUNCT_1:def 5;
         reconsider x as Element of B by A2,A7,XBOOLE_1:28;
         reconsider x'' = x as Element of B "\/" N
           by A1,GROUP_2:51;
         reconsider x' = x as Element of G by GROUP_2:51;
          A9: g.x = f.x' by A7,FUNCT_1:70
                 .= x' * N by Def9;
          then A10: g.x = N * x' by GROUP_3:140;
            x'' * (B "\/" N,N)`*` = x' * N & N * x' = (B "\/" N,N)`*`
 * x'' by A5,Th2;
          then y in I by A8,A9,A10,Th28;
       hence thesis by RLVECT_1:def 1;
      end;
    then reconsider g as Function of the carrier of B,
          the carrier of (B "\/" N)./.
(B "\/" N,N)`*` by A3,FUNCT_2:def 1,RELSET_1:11;
       now let a,b be Element of B;
       reconsider a' = a, b' = b as Element of G by GROUP_2:51;
        A11: f.a' = g.a & f.b' = g.b by FUNCT_1:72;
           a * b in the carrier of B & a * b = a' * b' &
             a' * b' in the carrier of G by GROUP_2:52;
      hence g.(a * b) = f.(a' * b') by FUNCT_1:72
                    .= f.a' * f.b' by Def7
                    .= g.a * g.b by A6,A11,GROUP_2:52;
     end;
    then reconsider g as Homomorphism of B,(B "\/" N)./.(B "\/"
 N,N)`*` by Def7;
    A12: Ker g = B /\ N
     proof let b be Element of B;
         reconsider c = b as Element of G by GROUP_2:51;
          A13: g.b = f.c by FUNCT_1:72
                      .= c * N by Def9;
      thus b in Ker g implies b in B /\ N
       proof assume b in Ker g;
          then g.b = 1.I by Th50
                  .= carr J by Th29
                  .= the carrier of N by A5,GROUP_2:def 9
                  .= carr N by GROUP_2:def 9;
          then b in B & b in N by A13,GROUP_2:136,RLVECT_1:def 1;
        hence thesis by GROUP_2:99;
       end;
       assume b in B /\ N;
        then b in N by GROUP_2:99;
        then c * N = carr N by GROUP_2:136
                  .= the carrier of J by A5,GROUP_2:def 9
                  .= carr J by GROUP_2:def 9
                  .= 1.I by Th29;
      hence thesis by A13,Th50;
     end;
      the carrier of I c= rng g
     proof let x;
       assume x in the carrier of I;
         then x in I by RLVECT_1:def 1;
        then consider b being Element of B "\/" N such that
         A14: x = b * J & x = J * b by Th28;
           B * N = N * B & b in B "\/" N by GROUP_5:8,RLVECT_1:def 1;
        then consider a1,a2 such that A15: b = a1 * a2 and A16: a1 in B & a2 in
 N
                                                                 by GROUP_5:5;
         A17: a1 in the carrier of B & a1 in the carrier of G by A16,RLVECT_1:
def 1;
           x = a1 * a2 * N by A5,A14,A15,Th2
          .= a1 * (a2 * N) by GROUP_2:127
          .= a1 * carr N by A16,GROUP_2:136
          .= a1 * N by GROUP_2:def 13
          .= f.a1 by Def9
          .= g.a1 by A17,FUNCT_1:72;
      hence thesis by A3,A17,FUNCT_1:def 5;
     end;
    then the carrier of I = rng g by XBOOLE_0:def 10;
    then g is_epimorphism by Def13;
    then Image g = (B "\/" N)./.(B "\/" N,N)`*` by Th67;
   hence thesis by A12,Lm9;
  end;

Back to top