Caves Travel Diving Graphics Mizar Texts Cuisine Lemkov Contact Map RSS Polski
Trybiks' Dive Mizar Articles Homomorphisms and Isomorphisms of Groups; Quotient Group YAC Software
  Back

Mizar

Eddie

Articles

Equivalence of Deterministic and Epsilon Nondeterministic Automata

Labelled State Transition Systems

Regular Expression Quantifiers - at least m Occurrences

String Rewriting Systems

Regular Expression Quantifiers - m to n Occurrences

Formal Languages- Concatenation and Closure

Boolean Properties of Sets

Homomorphisms and Isomorphisms of Groups; Quotient Group

Integers

Mizar-MSE Syntax

Homomorphisms and Isomorphisms of Groups; Quotient Group
Homomorphisms and isomorphisms of groups, and quotient group are introduced. The so called isomorphism theorems are proved following [1].

Bibliography:
[1] M. I. Kargapolow, J. I. Mierzlakow: "Introduction to Group Theory", PWN 1989.

Mizar Mathematical Library identifier: GROUP_6.
Article written with Wojciech Trybulec.
Abstract in PDF: here.
Warsaw University, 1991.

Files: Abstract
:: Homomorphisms and Isomorphisms of Groups. Quotient Group
::  by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991 Association of Mizar Users

environ

 vocabularies 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, FUNCOP_1, COHSP_1, NAT_1, ENDALG;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, NUMBERS, XXREAL_0,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
      CARD_1, FINSET_1, BINOP_1, REALSET2, INT_1, RLVECT_1, GROUP_1, GROUP_2,
      GROUP_3, NAT_1, NAT_D, GROUP_4, GROUP_5, INT_2;
 constructors RELAT_2, PARTFUN1, DOMAIN_1, BINOP_1, FUNCOP_1, FINSUB_1,
      XXREAL_0, NAT_1, INT_2, REALSET2, GROUP_4, GROUP_5, NAT_D;
 registrations FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1, INT_1,
      FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;

begin

theorem :: GROUP_6:1
  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;

definition let G be Group, A be Subgroup of G;
  redefine mode Subgroup of A -> Subgroup of G;
end;

registration let G be Group;
  cluster (1).G -> normal;
  cluster (Omega).G -> normal;
end;

 reserve n for Element of 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 :: GROUP_6:2
  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;

theorem :: GROUP_6:3
  for X,Y being Subgroup of A holds
  (X qua Subgroup of G) /\ (Y qua Subgroup of G) = X /\ Y;

theorem :: GROUP_6:4
  a * b * a" = b |^ a" & a * (b * a") = b |^ a";

canceled;

theorem :: GROUP_6:6
  a * A * A = a * A & a * (A * A) = a * A &
  A * A * a = A * a & A * (A * a) = A *a;

theorem :: GROUP_6:7
  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;

theorem :: GROUP_6:8
 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;

theorem :: GROUP_6:9
  for N being normal Subgroup of G holds
    N is Subgroup of B implies N is normal Subgroup of B;

definition let G,B; let M be normal Subgroup of G;
  assume  the HGrStr of M is Subgroup of B;
  func (B,M)`*` -> strict normal Subgroup of B equals
:: GROUP_6:def 1
    the HGrStr of M;
end;

theorem :: GROUP_6:10
  B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B;

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

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

definition let G be non empty 1-sorted;
  redefine attr G is trivial means
:: GROUP_6:def 2
  ex x st the carrier of G = {x};
end;

registration
  cluster trivial Group;
end;

theorem :: GROUP_6:11
  (1).G is trivial;

theorem :: GROUP_6:12
  G is trivial iff ord G = 1 & G is finite;

theorem :: GROUP_6:13
  for G being strict Group holds
    G is trivial implies (1).G = G;

definition let G,N;
  func Cosets N -> set equals
:: GROUP_6:def 3
    Left_Cosets N;
end;

registration let G,N;
  cluster Cosets N -> non empty;
end;

canceled;

theorem :: GROUP_6:15
 for N being normal Subgroup of G holds
 x in Cosets N implies ex a st x = a * N & x = N * a;

theorem :: GROUP_6:16
 for N being normal Subgroup of G holds
 a * N in Cosets N & N * a in Cosets N;

theorem :: GROUP_6:17
 for N being normal Subgroup of G holds
 x in Cosets N implies x is Subset of G;

theorem :: GROUP_6:18
 for N being normal Subgroup of G holds
 A1 in Cosets N & A2 in Cosets N implies A1 * A2 in Cosets N;

definition let G; let N be normal Subgroup of G;
  func CosOp N -> BinOp of Cosets N means
:: GROUP_6:def 4
   for W1,W2 being Element of Cosets N
     for A1,A2 st W1 = A1 & W2 = A2 holds it.(W1,W2) = A1 * A2;
end;

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

registration let G; let N be normal Subgroup of G;
  cluster G./.N -> strict non empty;
end;

canceled 3;

theorem :: GROUP_6:22
  for N being normal Subgroup of G holds
    the carrier of G./.N = Cosets N;

theorem :: GROUP_6:23
  for N being normal Subgroup of G holds
    the mult of G./.N = CosOp N;

 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
:: GROUP_6:def 6
S;
end;

theorem :: GROUP_6:24
  for N being normal Subgroup of G, T1,T2 being Element of G./.N
    holds @T1 * @T2 = T1 * T2;

theorem :: GROUP_6:25
  @(T1 * T2) = @T1 * @T2;

registration let G; let N be normal Subgroup of G;
  cluster G./.N -> associative Group-like;
end;

theorem :: GROUP_6:26
  for N being normal Subgroup of G, S being Element of G./.N
    ex a st S = a * N & S = N * a;

theorem :: GROUP_6:27
  N * a is Element of G./.N &
    a * N is Element of G./.N &
  carr N is Element of G./.N;

theorem :: GROUP_6:28
  for N being normal Subgroup of G holds
    x in G./.N iff ex a st x = a * N & x = N * a;

theorem :: GROUP_6:29
  for N being normal Subgroup of G holds
    1_(G./.N) = carr N;

theorem :: GROUP_6:30
  for N being normal Subgroup of G, S being Element of G./.N
    st S = a * N holds S" = a" * N;

canceled;

theorem :: GROUP_6:32
  for N being normal Subgroup of G holds
    Ord(G./.N) = Index N;

theorem :: GROUP_6:33
  for N being normal Subgroup of G holds
 Left_Cosets N is finite implies ord(G./.N) = index N;

theorem :: GROUP_6:34
 for M being strict normal Subgroup of G holds
 M is Subgroup of B implies B./.(B,M)`*` is Subgroup of G./.M;

theorem :: GROUP_6:35
    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;

theorem :: GROUP_6:36
  for G being strict Group, N be strict normal Subgroup of G holds
    G./.N is commutative Group iff G` is Subgroup of N;

definition let G, H be non empty HGrStr; let f be Function of G, H;
  attr f is multiplicative means
:: GROUP_6:def 7
    for a, b being Element of G holds f.(a * b) = f.a * f.b;
end;

registration let G, H;
  cluster multiplicative Function of G, H;
end;

definition let G,H;
  mode Homomorphism of G,H is multiplicative Function of G, H;
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 :: GROUP_6:40
  g.(1_G) = 1_H;

registration let G,H;
  cluster -> unity-preserving Homomorphism of G,H;
end;

theorem :: GROUP_6:41
  g.(a") = (g.a)";

theorem :: GROUP_6:42
  g.(a |^ b) = (g.a) |^ (g.b);

theorem :: GROUP_6:43
  g. [.a,b.] = [.g.a,g.b.];

theorem :: GROUP_6:44
  g. [.a1,a2,a3.] = [.g.a1,g.a2,g.a3.];

theorem :: GROUP_6:45
  g.(a |^ n) = (g.a) |^ n;

theorem :: GROUP_6:46
  g.(a |^ i) = (g.a) |^ i;

theorem :: GROUP_6:47
  id the carrier of G is Homomorphism of G,G;

theorem :: GROUP_6:48
  h1 * h is Homomorphism of G,I;

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

definition let G,H;
  func 1:(G,H) -> Homomorphism of G,H means
:: GROUP_6:def 8
   for a holds it.a = 1_H;
end;

theorem :: GROUP_6:49
  h1 * 1:(G,H) = 1:(G,I) & 1:(H,I) * h = 1:(G,I);

definition let G; let N be normal Subgroup of G;
  func nat_hom N -> Homomorphism of G,G./.N means
:: GROUP_6:def 9
   for a holds it.a = a * N;
end;

definition let G,H,g;
  func Ker g -> strict Subgroup of G means
:: GROUP_6:def 10
   the carrier of it = {a : g.a = 1_H};
end;

registration let G,H,g;
  cluster Ker g -> normal;
end;

theorem :: GROUP_6:50
  a in Ker h iff h.a = 1_H;

theorem :: GROUP_6:51
  for G,H being strict Group holds
    Ker 1:(G,H) = G;

theorem :: GROUP_6:52
  for N being strict normal Subgroup of G holds
    Ker nat_hom N = N;

definition let G,H,g;
  func Image g -> strict Subgroup of H means
:: GROUP_6:def 11
   the carrier of it = g .: (the carrier of G);
end;

theorem :: GROUP_6:53
  rng g = the carrier of Image g;

theorem :: GROUP_6:54
  x in Image g iff ex a st x = g.a;

theorem :: GROUP_6:55
  Image g = gr rng g;

theorem :: GROUP_6:56
  Image 1:(G,H) = (1).H;

theorem :: GROUP_6:57
  for N being normal Subgroup of G holds
    Image nat_hom N = G./.N;

theorem :: GROUP_6:58
  h is Homomorphism of G,Image h;

theorem :: GROUP_6:59
  G is finite implies Image g is finite;

theorem :: GROUP_6:60
  G is commutative Group implies Image g is commutative;

theorem :: GROUP_6:61
  Ord Image g <=` Ord G;

theorem :: GROUP_6:62
  G is finite implies ord Image g <= ord G;

definition let G,H,h;
  attr h is being_monomorphism means
:: GROUP_6:def 12
    h is one-to-one;
  attr h is being_epimorphism means
:: GROUP_6:def 13
    rng h = the carrier of H;
end;

notation let G,H,h;
  synonym h is_monomorphism for h is being_monomorphism;
  synonym h is_epimorphism for h is being_epimorphism;
end;

theorem :: GROUP_6:63
  h is_monomorphism & c in Image h implies h.(h".c) = c;

theorem :: GROUP_6:64
  h is_monomorphism implies h".(h.a) = a;

theorem :: GROUP_6:65
  h is_monomorphism implies h" is Homomorphism of Image h,G;

theorem :: GROUP_6:66
  h is_monomorphism iff Ker h = (1).G;

theorem :: GROUP_6:67
  for H being strict Group, h being Homomorphism of G,H holds
    h is_epimorphism iff Image h = H;

theorem :: GROUP_6:68
  for H being strict Group, h being Homomorphism of G,H st
    h is_epimorphism holds
      for c being Element of H ex a st h.a = c;

theorem :: GROUP_6:69
  for N being normal Subgroup of G holds
    nat_hom N is_epimorphism;

definition let G,H,h;
  attr h is being_isomorphism means
:: GROUP_6:def 14
    h is_epimorphism & h is_monomorphism;
end;

notation let G,H,h;
  synonym h is_isomorphism for h is being_isomorphism;
end;

theorem :: GROUP_6:70
  h is_isomorphism iff rng h = the carrier of H & h is one-to-one;

theorem :: GROUP_6:71
  h is_isomorphism implies dom h = the carrier of G &
    rng h = the carrier of H;

theorem :: GROUP_6:72
  for H being strict Group, h being Homomorphism of G,H st
    h is_isomorphism holds h" is Homomorphism of H,G;

theorem :: GROUP_6:73
  h is_isomorphism & g1 = h" implies g1 is_isomorphism;

theorem :: GROUP_6:74
  h is_isomorphism & h1 is_isomorphism implies h1 * h is_isomorphism;

theorem :: GROUP_6:75
  for G being Group holds
    nat_hom (1).G is_isomorphism;

definition let G,H;
  pred G,H are_isomorphic means
:: GROUP_6:def 15
    ex h st h is_isomorphism;
  reflexivity;
end;

canceled;

theorem :: GROUP_6:77
  for G,H being strict Group holds
    G,H are_isomorphic implies H,G are_isomorphic;

definition let G,H be strict Group;
  redefine pred G,H are_isomorphic;
  symmetry;
end;

theorem :: GROUP_6:78
  G,H are_isomorphic & H,I are_isomorphic implies G,I are_isomorphic;

theorem :: GROUP_6:79
  h is_monomorphism implies G,Image h are_isomorphic;

theorem :: GROUP_6:80
  for G,H being strict Group holds
    G is trivial & H is trivial implies G,H are_isomorphic;

theorem :: GROUP_6:81
  (1).G,(1).H are_isomorphic;

theorem :: GROUP_6:82
  for G being strict Group holds
    G,G./.(1).G are_isomorphic;

theorem :: GROUP_6:83
  for G being Group holds
    G./.(Omega).G is trivial;

theorem :: GROUP_6:84
  for G,H being strict Group holds
    G,H are_isomorphic implies Ord G = Ord H;

theorem :: GROUP_6:85
  G,H are_isomorphic & G is finite implies H is finite;

theorem :: GROUP_6:86
  for G,H being strict Group holds
    G,H are_isomorphic & G is finite implies ord G = ord H;

theorem :: GROUP_6:87
  for G,H being strict Group holds
    G,H are_isomorphic & G is trivial implies H is trivial;

canceled;

theorem :: GROUP_6:89
  for H being strict Group st
    G,H are_isomorphic & G is commutative Group holds H is commutative Group;

theorem :: GROUP_6:90
  G./.Ker g, Image g are_isomorphic;

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

theorem :: GROUP_6:92
  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;

theorem :: GROUP_6:93
  for N being strict normal Subgroup of G holds
(B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic;


Top

Full article
:: Homomorphisms and Isomorphisms of Groups. Quotient Group
::  by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991 Association of Mizar Users

environ

 vocabularies 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, FUNCOP_1, COHSP_1, NAT_1, ENDALG;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, NUMBERS, XXREAL_0,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, STRUCT_0,
      CARD_1, FINSET_1, BINOP_1, REALSET2, INT_1, RLVECT_1, GROUP_1, GROUP_2,
      GROUP_3, NAT_1, NAT_D, GROUP_4, GROUP_5, INT_2;
 constructors RELAT_2, PARTFUN1, DOMAIN_1, BINOP_1, FUNCOP_1, FINSUB_1,
      XXREAL_0, NAT_1, INT_2, REALSET2, GROUP_4, GROUP_5, NAT_D;
 registrations FINSET_1, GROUP_1, GROUP_2, GROUP_3, STRUCT_0, RELSET_1, INT_1,
      FUNCT_2, PARTFUN1, XBOOLE_0;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions XBOOLE_0, FUNCT_1, GROUP_1, GROUP_2, TARSKI, BINOP_1, REALSET1,
      SUBSET_1, GROUP_4;
 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, REALSET2,
      RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1;
 schemes BINOP_1, 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 by GROUP_2:65;
end;

registration 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 Element of 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 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 GROUP_1:def 4;
  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 * A by GROUP_2:91;
   hence a * (A * A) = a * A by GROUP_4:60;
   thus A * A * a = A * a by GROUP_2:91;
   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 DOMAIN_1:sch 9;
         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;
    thus a * x = a * M
              .= M * a by GROUP_3:140
              .= x * a;
   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,REALSET2:def 7;
    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 REALSET2:def 7;
  end;
end;

registration
  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 14;
      then ex B being finite set st B = the carrier of G & ord G = card B
              by GROUP_1:def 15;
     hence thesis by A1,CARD_1:79,GROUP_1:def 14;
    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 15;
   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
    Left_Cosets N;
  coherence;
end;

registration let G,N;
  cluster Cosets N -> non empty;
  coherence by GROUP_2:165;
end;

 Lm1:
  for N being normal Subgroup of G holds
    Cosets N = Left_Cosets N & Cosets N = Right_Cosets N by GROUP_3:150;

canceled;

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;
   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,Lm1;
  end;

theorem Th17:
 for N being normal Subgroup of G holds
 x in Cosets N implies x is Subset of G;

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 * N) by GROUP_2:91
          .= a * b * N by GROUP_2:127;
   then A1 * A2 in Left_Cosets N by GROUP_2:def 15;
   hence thesis;
  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 BINOP_1:sch 3(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;
            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);
      hence o1.(x,y) = o2.(x,y);
     end;
   hence thesis by BINOP_1:1;
  end;
end;

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

registration let G; let N be normal Subgroup of G;
  cluster G./.N -> strict non empty;
  coherence;
end;

canceled 3;

theorem
  for N being normal Subgroup of G holds
    the carrier of G./.N = Cosets N;

theorem
  for N being normal Subgroup of G holds
    the mult of G./.N = CosOp N;

 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   S;
  coherence by Th17;
end;

theorem Th24:
  for N being normal Subgroup of G, T1,T2 being Element of G./.N
    holds @T1 * @T2 = T1 * T2 by Def4;

theorem Th25:
  @(T1 * T2) = @T1 * @T2 by Th24;

registration let G; let N be normal Subgroup of G;
  cluster G./.N -> associative Group-like;
  coherence
  proof
   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 A1: f = a * N & f = N * a by Th15;
      consider c being Element of G such that
       A2: h = c * N & h = N * c by Th15;
     thus f * (g * h) = @f * @(g * h) by Th24
                     .= (a * N) * (@g * @h) by A1,Th25
                     .= @f * @g * (c * N) by A1,A2,GROUP_2:14
                     .= @(f * g) * @h by A2,Th25
                     .= f * g * h by Th24;
    end;
 carr N in Left_Cosets N & Cosets N = Left_Cosets N
                                                by GROUP_2:165;
    then reconsider e = carr N as Element of G./.N;
   take e;
   let h be Element of G./.N;
    consider a such that A3: h = a * N & h = N * a by Th15;
     A4: @h = h & @e = e;
   thus h * e = @h * @e by Th24
             .= (a * N) * N by A3
             .= a * (N * N) by GROUP_4:60
             .= h by  GROUP_2:91,A3;
   thus e * h = @e * @h by Th24
             .= N * (N * a) by A3
             .= N * N * a by GROUP_4:61
             .= h by  GROUP_2:91,A3;
    reconsider g = a" * N as Element of G./.N by GROUP_2:def 15;
     A5: @g = g;
   take g;
   thus h * g = N * a * (a" * N) by A3,A4,A5,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 6
             .= carr N * carr N by GROUP_2:132
             .= e by GROUP_2:91;
   thus g * h = @g * @h by Th24
             .= a" * N * a * N by 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 6
             .= 1_G * (N * N) by GROUP_4:60
             .= 1_G * carr N by GROUP_2:91
             .= 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 by Th15;

theorem Th27:
  N * a is Element of G./.N &
    a * N is Element of G./.N &
  carr N is Element of G./.N by Th16,GROUP_2:165;

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;
       now let h be Element of G./.N;
      consider a such that A1: h = a * N & h = N * a by Th15;
     thus h * e = @h * @e by Th24
               .= (a * N) * N by A1
               .= a * (N * N) by GROUP_4:60
               .= h by  GROUP_2:91,A1;
     thus e * h = @e * @h by Th24
               .= N * (N * a) by A1
               .= N * N * a by GROUP_4:61
               .= h by  GROUP_2:91,A1;
    end;
   hence thesis by GROUP_1:10;
  end;

theorem Th30:
  for N being normal Subgroup of G, S being Element of G./.N
    st S = a * N holds 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: S * g = @S * @g by Th24
              .= N * a * (a" * N) by A1,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 6
              .= carr N * carr N by GROUP_2:132
              .= carr N by GROUP_2:91;
     A3: g * S = @g * @S by Th24
              .= a" * N * a * N by A1,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 6
              .= 1_G * (N * N) by GROUP_4:60
              .= 1_G * carr N by GROUP_2:91
              .= carr N by GROUP_2:43;
   1_(G./.N) = carr N by Th29;
   hence thesis by A2,A3,GROUP_1:def 6;
  end;

 Lm2:
  for N being normal Subgroup of G holds
    Left_Cosets N is finite implies G./.N is finite by GROUP_1:def 14;

canceled;

theorem
  for N being normal Subgroup of G holds
    Ord(G./.N) = Index N;

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: G./.N is finite by A1,Lm2;
    then reconsider GN = the carrier of G./.N as finite set by GROUP_1:def 14;
   thus ord(G./.N) = card LC by A2,GROUP_1:def 15
                  .= 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;
         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;
       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 :];
      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 A5: dom g = dom f /\ X by XBOOLE_1:28;
        now let x;
       assume A6: x in dom g;
        then consider y,z such that A7: [y,z] = x by ZFMISC_1:102;
         A8: y in the carrier of I & z in
 the carrier of I by A6,A7,ZFMISC_1:106;
        consider a being Element of B such that
        A9: y = a * J & y = J * a by A8,Th15;
        consider b being Element of B such that
        A10: z = b * J & z = J * b by A8,Th15;
        reconsider W1 = y, W2 = z as Element of Cosets J by A9,A10,Th16;
         A11: g.x = g.(W1,W2) by A7
               .= (a * J) * (J * b) by A9,A10,Def4
               .= a * J * J * b by GROUP_3:12
               .= a * (J * J) * b by GROUP_4:60
               .= a * J * b by GROUP_2:91
               .= 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;
          A12: J = M by A1,Def1;
          then A13: y = a' * M & y = M * a' & z = b' * M & z = M * b' by A9
,A10,Th2;
         then reconsider V1 = y, V2 = z as Element of Cosets M by Th16;
          A14: f.x = f.(V1,V2) by A7
                .= (a' * M) * (M * b') by A13,Def4
               .= a' * M * M * b' by GROUP_3:12
               .= a' * (M * M) * b' by GROUP_4:60
               .= a' * M * b' by GROUP_2:91
               .= 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 A11,A12,A14,Th2;
     end;
     then g = f||the carrier of I by A5,FUNCT_1:68;
   hence B./.(B,M)`*` is Subgroup of G./.M 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 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 6
            .= 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_2:118
            .= M * (M * (a * (d * (a" * a)))) by GROUP_2:129
            .= M * (M * (a * (d * a" * a))) by GROUP_1:def 4
            .= M * (M * (a * (d * a") * a)) by GROUP_1:def 4
            .= 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 Th30;
         then A2: S" * T" = (a" * N) * (b" * N) by Th24;
            S = @S & T = @T;
         then A3: S * T = (a * N) * (b * N) by Th24;
         A4: @(S" * T") = (S" * T") & @(S * T) = (S * T);
            [.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,
Th30;
         then A9: S" * T" = (a" * N) * (b" * N) by Th24;
         S = @S & T = @T;
         then A10: S * T = (a * N) * (b * N) by A6,A7,Th24;
         A11: @(S" * T") = (S" * T") & @(S * T) = (S * T);
         [.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;

Lm3: (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 5
                 .= f.a * 1_H by A1
                 .= f.a * f.b by A1;
 end;

definition let G, H be non empty HGrStr; let f be Function of G, H;
  attr f is multiplicative means :Def7:
    for a, b being Element of G holds f.(a * b) = f.a * f.b;
end;

registration let G, H;
  cluster multiplicative Function of G, H;
  existence
  proof
   reconsider f = (the carrier of G) --> 1_H as Function of G, H
     by FUNCOP_1:57;
A1:for a holds f.a = 1_H by FUNCOP_1:13;
   take f;
   for a, b holds f.(a * b) = f.a * f.b by A1,Lm3;
   hence thesis by Def7;
  end;
end;

definition let G,H;
  mode Homomorphism of G,H is multiplicative Function of G, H;
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 5
               .= g.(1_G) * g.(1_G) by Def7;
   hence thesis by GROUP_1:15;
  end;

registration let G,H;
  cluster -> unity-preserving Homomorphism of G,H;
  coherence
  proof
    let g be Homomorphism of G,H;
    thus g.1_G = 1_H by Th40;
  end;
end;

theorem Th41:
  g.(a") = (g.a)"
  proof g.(a") * g.a = g.(a" * a) by Def7
                    .= g.(1_G) by GROUP_1:def 6
                    .= 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[Element of 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 NAT_1:sch 1(A1,A2);
   hence thesis;
  end;

theorem
  g.(a |^ i) = (g.a) |^ i
  proof
    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;
    end;
    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;
  end;

theorem Th47:
  id the carrier of G is Homomorphism of G,G
  proof
   reconsider f = id the carrier of G as Function of G, 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 G, 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;
  func 1:(G,H) -> Homomorphism of G,H means
  :Def8: for a holds it.a = 1_H;
 existence
  proof
   reconsider f = (the carrier of G) --> 1_H as Function of G, H
     by FUNCOP_1:57;
A1: for a holds f.a = 1_H by FUNCOP_1:13;
   f.(a * b) = f.a * f.b by A1,Lm3;
   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 FUNCT_1:sch 2
(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 G, 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;
      thus f.a * f.b = @(f.a) * @(f.b) by Th24
                    .= (a1 * N) * b1 * N by A8,A9,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_2:116
                    .= 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
    A11: for a holds n1.a = a * N and
    A12: for a holds n2.a = a * N;
       now let a;
         n1.a = a * N & n2.a = a * N by A11,A12;
     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 DOMAIN_1:sch 7;
        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 5;
      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;

registration 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 DOMAIN_1:sch 7;
     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 5;
      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;
   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 G, 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 G, 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 14;
   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 14;
  end;

Lm4: 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,Lm4
               .= 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 (g .: (the carrier of G)) by Def11;
   hence thesis by A1;
  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 15;
    consider ci being finite set such that
A4:  ci = the carrier of Image g & ord Image g = card ci by A2,GROUP_1:def 15;
      Ord Image g <=` Ord G by Th61;
   then Card (the carrier of Image g) <=` Ord G;
   then Card (the carrier of Image g) <=`
 Card (the carrier of G);
   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;
  attr h is being_epimorphism means :Def13:
    rng h = the carrier of H;
end;

notation let G,H,h;
  synonym h is_monomorphism for h is being_monomorphism;
  synonym h is_epimorphism for h is being_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 G,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 Imh,G
   proof
 A3: h is Function of G,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 Imh, G;
    now
    let a,b be Element of Imh;
    reconsider a' = a, 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 6
                .= 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 5
     .= b * a" * a by A4,A7,TARSKI:def 1
     .= b * (a" * a) by GROUP_1:def 4
     .= b * 1_G by GROUP_1:def 6
     .= b by GROUP_1:def 5;
    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 st
    h is_epimorphism holds
      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;
end;

notation let G,H,h;
  synonym h is_isomorphism for h is being_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 st
    h is_isomorphism holds 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;

definition let G,H be strict Group;
  redefine pred G,H are_isomorphic;
  symmetry by Th77;
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
  proof let G be strict Group;
   nat_hom (1).G is_isomorphism by Th75;
   hence G,G./.(1).G are_isomorphic by Def15;
  end;

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

theorem Th84:
  for G,H being strict Group holds
    G,H are_isomorphic implies Ord G = Ord H
  proof let G,H be strict Group;
   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;
   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;

theorem Th85:
  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 14;
   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 14;
  end;

theorem Th86:
  for G,H being strict Group holds
    G,H are_isomorphic & G 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;
      Ord G = Ord H by A1,Th84;
   then A3: Card (the carrier of G) = Card (the carrier of H);
A4: H is finite & G is finite by A1,A2,Th85;
    then consider cH being finite set such that
A5: cH = the carrier of H & ord H = card cH by GROUP_1:def 15;
    consider cG being finite set such that
A6: cG = the carrier of G & ord G = card cG by A4,GROUP_1:def 15;
   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,Th85;
   hence thesis by A4,Th12;
  end;

canceled;

theorem
  for H being strict Group st
    G,H are_isomorphic & G is commutative Group holds H is commutative Group
  proof let H be strict Group;
   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,Lm4
              .= d * c by A5,A6,Def7;
   end;
   hence thesis by GROUP_1:def 16;
  end;

Lm5:
 G./.Ker g,Image 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 I,J such that
     A3: for S being Element of I holds P[S,f.S] from FUNCT_2:sch 3(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;
        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;
         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 6;
        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;
   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 x in dom nat_hom Ker g & (nat_hom Ker g).x in dom f;
      hence x in dom g by A14;
     end;
     now let x;
      assume x in dom g;
      then reconsider a = x as Element of G;
      (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 by Lm5;

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

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 G./.M, G./.N
       such that A5: for x being Element of G./.M holds P[x,f.x]
                                               from FUNCT_2:sch 3(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 = a * N & f.y = b * N by A5,A6,A7;
          A9: f.x * f.y = @(f.x) * @(f.y) by Th24
                      .= a * N * b * N by A8,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_2:116
                      .= a * (b * N) by Th6
                      .= a * b * N by GROUP_2:127;
          x * y = @x * @y by Th24
               .= a * M * b * M by A6,A7,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_2:116
               .= a * (b * M) by Th6
               .= a * b * M by GROUP_2:127;
        hence f.(x * y) = f.x * f.y by A5,A9;
       end;
      then reconsider f as Homomorphism of G./.M,G./.N by Def7;
       A10: 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 A11: f.S = 1_(G./.N) by Th50
                        .= carr N by Th29;
            consider a such that A12: S = a * M & S = M * a by Th26;
                f.S = a * N by A5,A12;
             then a in N by A11,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 A12,Th2;
           hence thesis by A1,Th28;
          end;
          assume S in J;
           then consider a being Element of N such that
            A13: 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 A13,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 A14: 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 A14,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 A10,Lm5;
   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 B,
          (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
                  .= carr N by A5;
          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 J by A5,GROUP_2:136
                  .= 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 * N by A16,GROUP_2:136
          .= 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,Lm5;
end;


Top