:: Categories of Groups
::  by Michal Muzalewski
::
:: Received October 3, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, CLASSES2, TARSKI, ZFMISC_1, SUBSET_1, FUNCT_5, FUNCT_1,
      FUNCT_2, ALGSTR_0, MIDSP_2, ROBBINS1, SUPINF_2, ARYTM_3, ARYTM_1, CAT_1,
      STRUCT_0, RELAT_1, GRAPH_1, VECTSP_1, PARTFUN1, REALSET1, MIDSP_1, CAT_2,
      FUNCOP_1, MSSUBFAM, RLVECT_1, ENS_1, ALGSTR_1, GRCAT_1, MONOID_0,
      RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, MCART_1,
      REALSET1, PARTFUN1, FUNCT_2, ORDINAL1, CLASSES2, BINOP_1, FUNCOP_1,
      FUNCT_5,
      STRUCT_0, ALGSTR_0, GRAPH_1, CAT_1, TOPS_2, RLVECT_1, VECTSP_1,
      CAT_2, ALGSTR_1, MIDSP_2;
 constructors PARTFUN1, CLASSES1, CLASSES2, REALSET1, TOPS_2, VECTSP_2, CAT_2,
      ALGSTR_1, MIDSP_2, FUNCOP_1, RELSET_1, FUNCT_5, XTUPLE_0;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, CLASSES2, STRUCT_0, ALGSTR_1,
      MIDSP_2, ALGSTR_0, CAT_2, XTUPLE_0, CAT_1, REALSET1, SUBSET_1;
 requirements SUBSET, BOOLE;
 definitions BINOP_1, STRUCT_0, ALGSTR_1, ALGSTR_0, GRAPH_1, VECTSP_1, CAT_1,
      XTUPLE_0;
 theorems CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2, MCART_1,
      VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1, ORDINAL1, XBOOLE_0,
      TOPS_2, BINOP_1, CARD_1, SUBSET_1, XTUPLE_0;
 schemes FUNCT_2, BINOP_1, TARSKI, XBOOLE_0;

begin ::  0a. Auxiliary theorems: sets and universums

reserve x, y for set;
reserve D for non empty set;
reserve UN for Universe;

theorem Th1:
  for u1,u2,u3,u4 being Element of UN holds [u1,u2,u3] in UN & [u1,
  u2,u3,u4] in UN
proof
  let u1,u2,u3,u4 be Element of UN;
  [u1,u2,u3] = [[u1,u2],u3] & [u1,u2,u3,u4] = [[u1,u2,u3],u4];
  hence thesis by CLASSES2:58;
end;

::  0c. Auxiliary theorems: Trivial Group

theorem Th2:
  op2.({},{}) = {} & op1.{} = {} & op0 = {}
proof
  [{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
  hence op2.({},{}) = {} by CARD_1:49,FUNCT_2:50;
  {} in {{}} by TARSKI:def 1;
  hence op1.{} = {} by CARD_1:49,FUNCT_2:50;
  thus thesis;
end;

theorem Th3:
  {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN
proof
  set D = {{}};
  thus
A1: D in UN by CLASSES2:56,57;
  hence [D,D] in UN by CLASSES2:58;
A2: op2 in Funcs([:D,D:],D) by CARD_1:49,FUNCT_2:8;
  thus [:D,D:] in UN by A1,CLASSES2:61;
  then Funcs([:D,D:],D) in UN by A1,CLASSES2:61;
  hence op2 in UN by A2,ORDINAL1:10;
A3: op1 in Funcs(D,D) by CARD_1:49,FUNCT_2:8;
  Funcs(D,D) in UN by A1,CLASSES2:61;
  hence thesis by A3,ORDINAL1:10;
end;

registration
  cluster Trivial-addLoopStr -> midpoint_operator;
  coherence
proof
  set G = Trivial-addLoopStr;
A1: for a being Element of G ex x being Element of G st Double x = a
  proof
    set x = the Element of G;
    let a be Element of G;
    take x;
    thus Double x = {} by CARD_1:49,TARSKI:def 1
      .= a by CARD_1:49,TARSKI:def 1;
  end;
  for a being Element of G st Double a = 0.G holds a = 0.G by CARD_1:49
,TARSKI:def 1;
  hence thesis by A1,MIDSP_2:def 5;
end;
end;

theorem
  (for x being Element of Trivial-addLoopStr holds x = {}) & (for x,y
  being Element of Trivial-addLoopStr holds x+y = {}) & (for x being Element of
  Trivial-addLoopStr holds -x = {}) & 0.Trivial-addLoopStr = {} by CARD_1:49
,TARSKI:def 1;

::  0d. Auxiliary theorems: subcategories

reserve C for Category;
reserve O for non empty Subset of the carrier of C;

definition
  let C,O;

  func Morphs(O) -> Subset of the carrier' of C equals
  union{Hom(a,b) where a
  is Object of C,b is Object of C : a in O & b in O};
  coherence by CAT_2:19;
end;

registration
  let C,O;
  cluster Morphs(O) -> non empty;
  coherence by CAT_2:19;
end;

definition
  let C,O;
  func dom(O) -> Function of Morphs(O),O equals
  (the Source of C)|Morphs(O);
  coherence by CAT_2:20;
  func cod(O) -> Function of Morphs(O),O equals
  (the Target of C)|Morphs(O);
  coherence by CAT_2:20;
  func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals
  (the Comp of C)||Morphs(O);
  coherence by CAT_2:20;
 canceled;
end;

definition
  let C,O;
  func cat(O) -> Subcategory of C equals
  CatStr (# O,Morphs(O),dom(O),cod(O),comp(O)#);
  coherence
  proof
    CatStr (# O,Morphs(O),dom(O),cod(O),comp(O)#)
    is full Subcategory of C by CAT_2:21;
    hence thesis;
  end;
end;

registration
  let C,O;
  cluster cat(O) -> strict;
  coherence;
end;

theorem
  the carrier of cat(O) = O;

::  1a. Maps of the carriers of groups

definition
  let G be non empty 1-sorted, H be non empty ZeroStr;

  func ZeroMap(G,H) -> Function of G,H equals
  (the carrier of G) --> 0.H;
  coherence;
end;

theorem Th6:
  comp Trivial-addLoopStr = op1
proof
  reconsider f = comp Trivial-addLoopStr as Function of {{}}, {{}} by CARD_1:49
;
  for x being set st x in {{}} holds op1.x = f.x
  proof
    let x be set;
    assume x in {{}};
    then reconsider x as Element of Trivial-addLoopStr by CARD_1:49;
    x = {} by CARD_1:49,TARSKI:def 1;
    then op1.x = -x by Th2,CARD_1:49,TARSKI:def 1
      .= f.x by VECTSP_1:def 13;
    hence thesis;
  end;
  hence thesis by CARD_1:49,FUNCT_2:12;
end;

registration
 let G be non empty addMagma, H being right_zeroed non empty addLoopStr;
 cluster ZeroMap(G,H) -> additive;
 coherence
proof
  set f = ZeroMap(G,H);
    let x,y be Element of G;
A1: f.y = 0.H by FUNCOP_1:7;
    f.(x+y) = 0.H & f.x = 0.H by FUNCOP_1:7;
    hence thesis by A1,RLVECT_1:def 4;
end;
end;

registration
 let G be non empty addMagma, H be right_zeroed non empty addLoopStr;
 cluster additive for Function of G,H;
 existence
  proof
   take ZeroMap(G,H);
   thus thesis;
  end;
end;

theorem Th7:
  for G1,G2,G3 being non empty addMagma, f being Function of G1,
  G2, g being Function of G2,G3 st f is additive & g is additive holds g*f is
  additive
proof
  let G1,G2,G3 be non empty addMagma, f be Function of G1,G2, g be Function
  of G2,G3 such that
A1: f is additive and
A2: g is additive;
  set h = g*f;
  now
    let x,y be Element of G1;
A3: g.(f.x) = h.x & g.(f.y) = h.y by FUNCT_2:15;
    thus h.(x+y) = g.(f.(x+y)) by FUNCT_2:15
      .= g.(f.x+f.y) by A1,VECTSP_1:def 20
      .= h.x+h.y by A2,A3,VECTSP_1:def 20;
  end;
  hence thesis by VECTSP_1:def 20;
end;

registration
 let G1 be non empty addMagma,
     G2,G3 being right_zeroed non empty addLoopStr,
     f being additive Function of G1, G2,
     g being additive Function of G2, G3;
 cluster g*f -> additive for Function of G1, G3;
 coherence by Th7;
end;

::  1b. carrier of groups

reserve G,H for AddGroup;

definition
  struct GroupMorphismStr (# Source,Target -> AddGroup, Fun -> Function of the
    Source, the Target #);
end;

definition
 canceled;
  let f be GroupMorphismStr;
  func dom(f) -> AddGroup equals
  the Source of f;
  coherence;
  func cod(f) -> AddGroup equals
  the Target of f;
  coherence;
end;

definition
  let f be GroupMorphismStr;
  func fun(f) -> Function of dom(f),cod(f) equals
  the Fun of f;
  coherence;
end;

theorem
  for f being GroupMorphismStr, G1,G2 being AddGroup, f0 being Function
  of G1,G2 st f = GroupMorphismStr(# G1,G2,f0#) holds dom f = G1 & cod f = G2 &
  fun f = f0;

definition
  let G,H;
  func ZERO(G,H) -> GroupMorphismStr equals
  GroupMorphismStr(# G,H,ZeroMap(G,H)#);
  coherence;
end;

registration
  let G,H;
  cluster ZERO(G,H) -> strict;
  coherence;
end;

definition
  let IT be GroupMorphismStr;
  attr IT is GroupMorphism-like means
  :Def13:
  fun(IT) is additive;
end;

registration
  cluster strict GroupMorphism-like for GroupMorphismStr;
  existence
  proof
    set G = the AddGroup;
    set z = ZERO(G,G);
    fun(z) is additive;
    then z is GroupMorphism-like by Def13;
    hence thesis;
  end;
end;

definition
  mode GroupMorphism is GroupMorphism-like GroupMorphismStr;
end;

theorem Th9:
  for F being GroupMorphism holds the Fun of F is additive
proof
  let F be GroupMorphism;
  the Fun of F = fun(F);
  hence thesis by Def13;
end;

registration
  let G,H;
  cluster ZERO(G,H) -> GroupMorphism-like;
  coherence
  proof
    set z = ZERO(G,H);
    fun(z) is additive;
    hence thesis by Def13;
  end;
end;

definition
  let G,H;
  mode Morphism of G,H -> GroupMorphism means
    :Def14:
    dom(it) = G & cod(it) = H;
  existence
  proof
    take ZERO(G,H);
    thus thesis;
  end;
end;

registration
  let G,H;
  cluster strict for Morphism of G,H;
  existence
  proof
    dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H;
    then ZERO(G,H) is Morphism of G,H by Def14;
    hence thesis;
  end;
end;

theorem Th10:
  for f being strict GroupMorphismStr st dom(f) = G & cod(f) = H &
  fun(f) is additive holds f is strict Morphism of G,H
proof
  let f be strict GroupMorphismStr;
  assume that
A1: dom(f) = G & cod(f) = H and
A2: fun(f) is additive;
  reconsider f9 = f as strict GroupMorphism by A2,Def13;
  f9 is strict Morphism of G,H by A1,Def14;
  hence thesis;
end;

theorem Th11:
  for f being Function of G,H st f is additive holds
  GroupMorphismStr (# G,H,f#) is strict Morphism of G,H
proof
  let f be Function of G,H such that
A1: f is additive;
  set F = GroupMorphismStr (# G,H,f#);
  fun(F) = f;
  hence thesis by A1,Th10;
end;

registration let G be non empty addMagma;
 cluster id G -> additive;
 coherence
proof
  set f = id G;
    let x,y be Element of G;
    f.(x+y) = x+y & f.x = x by FUNCT_1:18;
    hence thesis by FUNCT_1:18;
end;
end;

definition
  let G;
  func ID G -> Morphism of G,G equals
  GroupMorphismStr(# G,G,id G#);
  coherence
  proof
    set i = GroupMorphismStr(# G,G,id G#);
    fun(i) = id G;
    hence thesis by Th10;
  end;
end;

registration
  let G;
  cluster ID G -> strict;
  coherence;
end;

definition
  let G,H;
  redefine func ZERO(G,H) -> strict Morphism of G,H;
  coherence
  proof
    set i = ZERO(G,H);
    fun(i) = ZeroMap(G,H);
    hence thesis by Th10;
  end;
end;

theorem Th12:
  for F being Morphism of G,H ex f being Function of G,H st the
  GroupMorphismStr of F = GroupMorphismStr(# G,H,f#) & f is additive
proof
  let F be Morphism of G,H;
A1: the Target of F = cod(F) .= H by Def14;
A2: the Source of F = dom(F) .= G by Def14;
  then reconsider f = the Fun of F as Function of G,H by A1;
  take f;
  thus thesis by A2,A1,Th9;
end;

theorem Th13:
  for F being strict Morphism of G,H ex f being Function of G,H st
  F = GroupMorphismStr(# G,H,f#)
proof
  let F be strict Morphism of G,H;
  consider f being Function of G,H such that
A1: F = GroupMorphismStr(# G,H,f#) and
  f is additive by Th12;
  take f;
  thus thesis by A1;
end;

theorem Th14:
  for F being GroupMorphism ex G,H st F is Morphism of G,H
proof
  let F be GroupMorphism;
  take G = the Source of F,H = the Target of F;
  dom(F) = G & cod(F) = H;
  hence thesis by Def14;
end;

theorem
  for F being strict GroupMorphism ex G,H being AddGroup, f being
Function of G,H st F is Morphism of G,H & F = GroupMorphismStr(# G,H,f#) & f is
  additive
proof
  let F be strict GroupMorphism;
  consider G,H such that
A1: F is Morphism of G,H by Th14;
  reconsider F9 = F as Morphism of G,H by A1;
  consider f being Function of G,H such that
A2: F9 = GroupMorphismStr(# G,H,f#) & f is additive by Th12;
  take G,H,f;
  thus thesis by A2;
end;

theorem Th16:
  for g,f being GroupMorphism st dom(g) = cod(f) ex G1,G2,G3 being
  AddGroup st g is Morphism of G2,G3 & f is Morphism of G1,G2
proof
  defpred P[GroupMorphism,GroupMorphism] means dom($1) = cod($2);
  let g,f be GroupMorphism such that
A1: P[g,f];
  consider G2,G3 being AddGroup such that
A2: g is Morphism of G2,G3 by Th14;
  consider G1,G29 being AddGroup such that
A3: f is Morphism of G1,G29 by Th14;
A4: G29 = cod(f) by A3,Def14;
  G2 = dom(g) by A2,Def14;
  hence thesis by A1,A2,A3,A4;
end;

definition
  let G,F be GroupMorphism;
  assume
A1: dom(G) = cod(F);
  func G*F -> strict GroupMorphism means
  :Def16:
  for G1,G2,G3 being AddGroup,
g being Function of G2,G3, f being Function of G1,G2 st the GroupMorphismStr of
G = GroupMorphismStr(# G2,G3,g#) & the GroupMorphismStr of F = GroupMorphismStr
  (# G1,G2,f#) holds it = GroupMorphismStr(# G1,G3,g*f#);
  existence
  proof
    consider G19,G29,G39 being AddGroup such that
A2: G is Morphism of G29,G39 and
A3: F is Morphism of G19,G29 by A1,Th16;
    consider f9 being Function of G19,G29 such that
A4: the GroupMorphismStr of F = GroupMorphismStr(# G19,G29,f9#) and
A5: f9 is additive by A3,Th12;
    consider g9 being Function of G29,G39 such that
A6: the GroupMorphismStr of G = GroupMorphismStr(# G29,G39,g9#) and
A7: g9 is additive by A2,Th12;
    g9*f9 is additive by A7,A5;
    then reconsider T9 = (GroupMorphismStr(# G19,G39,g9*f9#)) as strict
    GroupMorphism by Th11;
    take T9;
    thus thesis by A6,A4;
  end;
  uniqueness
  proof
    consider G19,G299 being AddGroup such that
A8: F is Morphism of G19,G299 by Th14;
    reconsider F9 = F as Morphism of G19,G299 by A8;
    consider G29,G39 being AddGroup such that
A9: G is Morphism of G29,G39 by Th14;
    G29 = dom(G) by A9,Def14;
    then reconsider F9 as Morphism of G19,G29 by A1,Def14;
    consider f9 being Function of G19,G29 such that
A10: the GroupMorphismStr of F9 = GroupMorphismStr(# G19,G29,f9#) and
    f9 is additive by Th12;
    reconsider G9 = G as Morphism of G29,G39 by A9;
    let S1,S2 be strict GroupMorphism such that
A11: for G1,G2,G3 being AddGroup, g being Function of G2,G3, f being
Function of G1,G2 st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
    the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) holds S1 =
    GroupMorphismStr(# G1,G3,g*f#) and
A12: for G1,G2,G3 being AddGroup, g being Function of G2,G3, f being
Function of G1,G2 st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) &
    the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) holds S2 =
    GroupMorphismStr(# G1,G3,g*f#);
    consider g9 being Function of G29,G39 such that
A13: the GroupMorphismStr of G9 = GroupMorphismStr(# G29,G39,g9#) and
    g9 is additive by Th12;
    thus S1 = (GroupMorphismStr(# G19,G39,g9*f9#)) by A11,A13,A10
      .= S2 by A12,A13,A10;
  end;
end;

theorem Th17:
  for G1,G2,G3 being AddGroup, G being Morphism of G2,G3, F being
  Morphism of G1,G2 holds G*F is Morphism of G1,G3
proof
  let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2;
  consider g being Function of G2,G3 such that
A1: the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) and
  g is additive by Th12;
  consider f being Function of G1,G2 such that
A2: the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) and
  f is additive by Th12;
  dom(G) = G2 by Def14
    .= cod(F) by Def14;
  then G*F = GroupMorphismStr(# G1,G3,g*f#) by A1,A2,Def16;
  then dom(G*F) = G1 & cod(G*F) = G3;
  hence thesis by Def14;
end;

definition
  let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2;
  redefine func G*F -> strict Morphism of G1,G3;
  coherence by Th17;
end;

theorem Th18:
  for G1,G2,G3 being AddGroup, G being Morphism of G2,G3, F being
Morphism of G1,G2, g being Function of G2,G3, f being Function of G1,G2 st G =
  GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#) holds G*F =
  GroupMorphismStr(# G1,G3,g*f#)
proof
  let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2, g
  be Function of G2,G3, f be Function of G1,G2 such that
A1: G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#);
  dom(G) = G2 by Def14
    .= cod(F) by Def14;
  hence thesis by A1,Def16;
end;

theorem Th19:
  for f,g being strict GroupMorphism st dom g = cod f holds ex G1,
G2,G3 being AddGroup, f0 being Function of G1,G2, g0 being Function of G2,G3 st
  f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0#) & g*f =
  GroupMorphismStr(# G1,G3,g0*f0#)
proof
  let f,g be strict GroupMorphism such that
A1: dom g = cod f;
  set G1 = dom f,G2 = cod f, G3 = cod g;
  reconsider f9 = f as strict Morphism of G1,G2 by Def14;
  reconsider g9 = g as strict Morphism of G2,G3 by A1,Def14;
  consider f0 being Function of G1,G2 such that
A2: f9 = GroupMorphismStr(# G1,G2,f0#);
  consider g0 being Function of G2,G3 such that
A3: g9 = GroupMorphismStr(# G2,G3,g0#) by Th13;
  take G1,G2,G3,f0,g0;
  thus thesis by A2,A3,Th18;
end;

theorem Th20:
  for f,g being strict GroupMorphism st dom g = cod f holds dom(g*
  f) = dom f & cod (g*f) = cod g
proof
  let f,g be strict GroupMorphism;
  assume dom g = cod f;
  then
A1: ex G1,G2,G3 being AddGroup, f0 being Function of G1,G2, g0 being Function
of G2,G3 st f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0
  #) & g*f = GroupMorphismStr(# G1,G3,g0*f0#) by Th19;
  hence dom(g*f) = dom f;
  thus thesis by A1;
end;

theorem Th21:
  for G1,G2,G3,G4 being AddGroup, f being strict Morphism of G1,G2
, g being strict Morphism of G2,G3, h being strict Morphism of G3,G4 holds h*(g
  *f) = (h*g)*f
proof
  let G1,G2,G3,G4 be AddGroup, f be strict Morphism of G1,G2, g be strict
  Morphism of G2,G3, h be strict Morphism of G3,G4;
  consider f0 being Function of G1,G2 such that
A1: f = GroupMorphismStr(# G1,G2,f0#) by Th13;
  consider g0 being Function of G2,G3 such that
A2: g = GroupMorphismStr(# G2,G3,g0#) by Th13;
  consider h0 being Function of G3,G4 such that
A3: h = GroupMorphismStr(# G3,G4,h0#) by Th13;
A4: h*g = GroupMorphismStr(# G2,G4,h0*g0#) by A2,A3,Th18;
  g*f = GroupMorphismStr(# G1,G3,g0*f0#) by A1,A2,Th18;
  then h*(g*f) = GroupMorphismStr(# G1,G4,h0*(g0*f0)#) by A3,Th18
    .= GroupMorphismStr(# G1,G4,(h0*g0)*f0#) by RELAT_1:36
    .= (h*g)*f by A1,A4,Th18;
  hence thesis;
end;

theorem Th22:
  for f,g,h being strict GroupMorphism st dom h = cod g & dom g =
  cod f holds h*(g*f) = (h*g)*f
proof
  let f,g,h be strict GroupMorphism such that
A1: dom h = cod g and
A2: dom g = cod f;
  set G2 = cod f, G3 = cod g;
  reconsider h9 = h as Morphism of G3,(cod h) by A1,Def14;
  reconsider g9 = g as Morphism of G2,G3 by A2,Def14;
  reconsider f9 = f as Morphism of (dom f),G2 by Def14;
  h9*(g9*f9) = (h9*g9)*f9 by Th21;
  hence thesis;
end;

theorem
  dom ID(G) = G & cod ID(G) = G & (for f being strict
  GroupMorphism st cod f = G holds (ID G)*f = f) & for g being strict
  GroupMorphism st dom g = G holds g*(ID G) = g
proof
  set i = ID G;
  thus dom i = G;
  thus cod i = G;
  thus for f being strict GroupMorphism st cod f = G holds i*f = f
  proof
    let f be strict GroupMorphism such that
A1: cod f = G;
    set H = dom(f);
    reconsider f9 = f as Morphism of H,G by A1,Def14;
    consider m being Function of H,G such that
A2: f9 = GroupMorphismStr(# H,G,m#) by Th13;
    dom(i) = G & (id G)*m = m by FUNCT_2:17;
    hence thesis by A1,A2,Def16;
  end;
  thus for g being strict GroupMorphism st dom g = G holds g*(ID G) = g
  proof
    let f be strict GroupMorphism such that
A3: dom f = G;
    set H = cod(f);
    reconsider f9 = f as Morphism of G,H by A3,Def14;
    consider m being Function of G,H such that
A4: f9 = GroupMorphismStr(# G,H,m#) by Th13;
    cod(i) = G & m*(id G) = m by FUNCT_2:17;
    hence thesis by A3,A4,Def16;
  end;
end;

::  2. Sourceains of groups

definition
  let IT be set;
  attr IT is Group_DOMAIN-like means
  :Def17:
  for x being set st x in IT holds x is strict AddGroup;
end;

registration
  cluster Group_DOMAIN-like non empty for set;
  existence
  proof
    set D = {Trivial-addLoopStr};
    take D;
    for x be set st x in D holds x is strict AddGroup by TARSKI:def 1;
    hence thesis by Def17;
  end;
end;

definition
  mode Group_DOMAIN is Group_DOMAIN-like non empty set;
end;

reserve V for Group_DOMAIN;

definition
  let V;
  redefine mode Element of V -> AddGroup;
  coherence by Def17;
end;

registration
  let V;
  cluster strict for Element of V;
  existence
  proof
    set v = the Element of V;
    v is strict AddGroup by Def17;
    hence thesis;
  end;
end;

::  3. Domains of morphisms

definition
  let IT be set;
  attr IT is GroupMorphism_DOMAIN-like means
  :Def18:
  for x being set st x in IT holds x is strict GroupMorphism;
end;

registration
  cluster GroupMorphism_DOMAIN-like non empty for set;
  existence
  proof
    set G = the AddGroup;
    take {ID G};
    for x being set st x in {ID G} holds x is strict GroupMorphism by
TARSKI:def 1;
    hence thesis by Def18;
  end;
end;

definition
  mode GroupMorphism_DOMAIN is GroupMorphism_DOMAIN-like non empty set;
end;

definition
  let M be GroupMorphism_DOMAIN;
  redefine mode Element of M -> GroupMorphism;
  coherence by Def18;
end;

registration
  let M be GroupMorphism_DOMAIN;
  cluster strict for Element of M;
  existence
  proof
    set m = the Element of M;
    m is strict GroupMorphism by Def18;
    hence thesis;
  end;
end;

theorem Th24:
  for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
proof
  let f be strict GroupMorphism;
  for x being set st x in {f} holds x is strict GroupMorphism by TARSKI:def 1;
  hence thesis by Def18;
end;

definition
  let G,H;
  mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means
    :Def19:
    for x being Element of it holds x is strict Morphism of G,H;
  existence
  proof
    reconsider D = {ZERO(G,H)} as GroupMorphism_DOMAIN by Th24;
    take D;
    thus thesis by TARSKI:def 1;
  end;
end;

theorem Th25:
  D is GroupMorphism_DOMAIN of G,H iff for x being Element of D
  holds x is strict Morphism of G,H
proof
  thus D is GroupMorphism_DOMAIN of G,H implies for x being Element of D holds
  x is strict Morphism of G,H by Def19;
  thus (for x being Element of D holds x is strict Morphism of G,H) implies D
  is GroupMorphism_DOMAIN of G,H
  proof
    assume
A1: for x being Element of D holds x is strict Morphism of G,H;
    then for x being set st x in D holds x is strict GroupMorphism;
    then reconsider D9 = D as GroupMorphism_DOMAIN by Def18;
    for x being Element of D9 holds x is strict Morphism of G,H by A1;
    hence thesis by Def19;
  end;
end;

theorem
  for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G, H
proof
  let f be strict Morphism of G,H;
  for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def 1;
  hence thesis by Th25;
end;

definition
  let G,H be 1-sorted;
  mode MapsSet of G,H means
    :Def20:
    for x being set st x in it holds x is Function of G,H;
  existence
  proof
    take {};
    thus thesis;
  end;
end;

definition
  let G,H be 1-sorted;
  func Maps(G,H) -> MapsSet of G,H equals
  Funcs(the carrier of G, the carrier
  of H);
  coherence
  proof
    let x be set;
    assume x in Funcs(the carrier of G, the carrier of H);
    hence thesis by FUNCT_2:66;
  end;
end;

registration
  let G be 1-sorted, H be non empty 1-sorted;
  cluster Maps(G,H) -> non empty;
  coherence;
end;

registration
  let G be 1-sorted, H be non empty 1-sorted;
  cluster non empty for MapsSet of G,H;
  existence
  proof
    Maps(G,H) is non empty;
    hence thesis;
  end;
end;

definition
  let G be 1-sorted, H be non empty 1-sorted;
  let M be non empty MapsSet of G,H;
  redefine mode Element of M -> Function of G,H;
  coherence by Def20;
end;

definition
  let G,H;
  func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means
  :Def22:
  x in it iff x is strict Morphism of G,H;
  existence
  proof
    reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by FUNCT_2:8;
    set D = { GroupMorphismStr(# G,H,f#) where f is Element of Maps(G,H) : f
    is additive };
    GroupMorphismStr(# G,H,f0#) in D;
    then reconsider D as non empty set;
A1: x in D implies x is strict Morphism of G,H
    proof
      assume x in D;
      then
      ex f being Element of Maps(G,H) st x = GroupMorphismStr (# G,H,f#) &
      f is additive;
      hence thesis by Th11;
    end;
    then
A2: for x being Element of D holds x is strict Morphism of G,H;
A3: x is strict Morphism of G,H implies x in D
    proof
      assume x is strict Morphism of G,H;
      then reconsider x as strict Morphism of G,H;
A4:   dom(x) = G & cod(x) = H by Def14;
      then reconsider f = the Fun of x as Function of G,H;
      reconsider g = f as Element of Maps(G,H) by FUNCT_2:8;
A5:   x = GroupMorphismStr(# G,H,g #) by A4;
      (the Fun of x) is additive by Th9;
      hence thesis by A5;
    end;
    reconsider D as GroupMorphism_DOMAIN of G,H by A2,Th25;
    take D;
    thus thesis by A1,A3;
  end;
  uniqueness
  proof
    let D1,D2 be GroupMorphism_DOMAIN of G,H such that
A6: x in D1 iff x is strict Morphism of G,H and
A7: x in D2 iff x is strict Morphism of G,H;
    x in D1 iff x in D2
    proof
      thus x in D1 implies x in D2
      proof
        assume x in D1;
        then x is strict Morphism of G,H by A6;
        hence thesis by A7;
      end;
      thus x in D2 implies x in D1
      proof
        assume x in D2;
        then x is strict Morphism of G,H by A7;
        hence thesis by A6;
      end;
    end;
    hence thesis by TARSKI:1;
  end;
end;

definition
  let G,H;
  let M be GroupMorphism_DOMAIN of G,H;
  redefine mode Element of M -> Morphism of G,H;
  coherence by Def19;
end;

registration
  let G,H;
  let M be GroupMorphism_DOMAIN of G,H;
  cluster strict for Element of M;
  existence
  proof
    set m = the Element of M;
    m is strict Morphism of G,H by Def19;
    hence thesis;
  end;
end;

::  4a. Category of groups - objects

definition
  let x,y;
  pred GO x,y means
  :Def23:
  ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] & ex
G being strict AddGroup st y = G & x1 = the carrier of G & x2 = the addF of G &
  x3 = comp G & x4 = 0.G;
end;

theorem Th27:
  for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2
proof
  let x,y1,y2 be set such that
A1: GO x,y1 and
A2: GO x,y2;
  consider a1,a2,a3,a4 being set such that
A3: x = [a1,a2,a3,a4] and
A4: ex G being strict AddGroup st y1 = G & a1 = the carrier of G & a2 =
  the addF of G & a3 = comp G & a4 = 0.G by A1,Def23;
  consider G1 being strict AddGroup such that
A5: y1 = G1 and
A6: a1 = the carrier of G1 & a2 = the addF of G1 and
  a3 = comp G1 and
A7: a4 = 0.G1 by A4;
  consider b1,b2,b3,b4 being set such that
A8: x = [b1,b2,b3,b4] and
A9: ex G being strict AddGroup st y2 = G & b1 = the carrier of G & b2 =
  the addF of G & b3 = comp G & b4 = 0.G by A2,Def23;
  consider G2 being strict AddGroup such that
A10: y2 = G2 and
A11: b1 = the carrier of G2 & b2 = the addF of G2 and
  b3 = comp G2 and
A12: b4 = 0.G2 by A9;
  the carrier of G1 = the carrier of G2 & the addF of G1 = the addF of G2
  by A3,A8,A6,A11,XTUPLE_0:5;
  hence thesis by A3,A8,A5,A7,A10,A12,XTUPLE_0:5;
end;

theorem Th28:
  ex x st x in UN & GO x,Trivial-addLoopStr
proof
  reconsider x2 = op2 as Element of UN by Th3;
  reconsider x3 = comp Trivial-addLoopStr as Element of UN by Th3,Th6;
  reconsider u = {} as Element of UN by CLASSES2:56;
  set x1 = {u};
  Extract {} = u;
  then reconsider x4 = Extract {} as Element of UN;
  take x = [x1,x2,x3,x4];
  thus x in UN by Th1;
  take x1,x2,x3,x4;
  thus x = [x1,x2,x3,x4];
  take Trivial-addLoopStr;
  thus thesis by CARD_1:49;
end;

definition
  let UN;
  func GroupObjects(UN) -> set means
  :Def24:
  for y holds y in it iff ex x st x in UN & GO x,y;
  existence
  proof
    defpred P[set,set] means GO $1,$2;
A1: for x,y1,y2 being set st P[x,y1] & P[x,y2] holds y1 = y2 by Th27;
    consider Y being set such that
A2: for y holds y in Y iff ex x st x in UN & P[x,y] from TARSKI:sch 1(
    A1);
    take Y;
    thus thesis by A2;
  end;
  uniqueness
  proof
    defpred P[set] means ex x st x in UN & GO x,$1;
    for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
    x being set holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
    hence thesis;
  end;
end;

theorem Th29:
  Trivial-addLoopStr in GroupObjects(UN)
proof
  ex x st x in UN & GO x,Trivial-addLoopStr by Th28;
  hence thesis by Def24;
end;

registration
  let UN;
  cluster GroupObjects(UN) -> non empty;
  coherence by Th29;
end;

theorem Th30:
  for x being Element of GroupObjects(UN) holds x is strict AddGroup
proof
  let x be Element of GroupObjects(UN);
  consider u being set such that
  u in UN and
A1: GO u,x by Def24;
  ex x1,x2,x3,x4 being set st u = [x1,x2,x3,x4] & ex G being strict
AddGroup st x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G &
  x4 = 0.G by A1,Def23;
  hence thesis;
end;

registration
  let UN;
  cluster GroupObjects(UN) -> Group_DOMAIN-like;
  coherence
  proof let x;
   thus thesis by Th30;
  end;
end;

::  4b. Category of groups - morphisms

definition
  let V;
  func Morphs(V) -> GroupMorphism_DOMAIN means
  :Def25:
  for x holds x in it iff
  ex G,H being strict Element of V st x is strict Morphism of G,H;
  existence
  proof
    set G0 = the strict Element of V;
    set M = Morphs(G0,G0), S = { Morphs(G,H) where G is strict Element of V, H
    is strict Element of V : not contradiction };
    (ZERO(G0,G0)) is Element of M & M in S by Def22;
    then reconsider T = union S as non empty set by TARSKI:def 4;
A1: for x holds x in T iff ex G,H being strict Element of V st x is strict
    Morphism of G,H
    proof
      let x;
      thus x in T implies ex G,H being strict Element of V st x is strict
      Morphism of G,H
      proof
        assume x in T;
        then consider Y being set such that
A2:     x in Y and
A3:     Y in S by TARSKI:def 4;
        consider G,H being strict Element of V such that
A4:     Y = Morphs(G,H) by A3;
        take G,H;
        thus thesis by A2,A4,Def22;
      end;
      thus (ex G,H being strict Element of V st x is strict Morphism of G,H)
      implies x in T
      proof
        given G,H being strict Element of V such that
A5:     x is strict Morphism of G,H;
        set M = Morphs(G,H);
A6:     M in S;
        x in M by A5,Def22;
        hence thesis by A6,TARSKI:def 4;
      end;
    end;
    now
      let x be set;
      assume x in T;
      then ex G,H being strict Element of V st x is strict Morphism of G,H by
A1;
      hence x is strict GroupMorphism;
    end;
    then reconsider T9 = T as GroupMorphism_DOMAIN by Def18;
    take T9;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let D1,D2 be GroupMorphism_DOMAIN such that
A7: for x holds x in D1 iff ex G,H being strict Element of V st x is
    strict Morphism of G,H and
A8: for x holds x in D2 iff ex G,H being strict Element of V st x is
    strict Morphism of G,H;
    now
      let x;
      x in D1 iff ex G,H being strict Element of V st x is strict
      Morphism of G,H by A7;
      hence x in D1 iff x in D2 by A8;
    end;
    hence thesis by TARSKI:1;
  end;
end;

::
::  4c. Category of groups - dom,cod,id
::

definition
  let V;
  let F be Element of Morphs(V);
  redefine func dom(F) -> strict Element of V;
  coherence
  proof
    consider G,H being strict Element of V such that
A1: F is strict Morphism of G,H by Def25;
    reconsider F9 = F as Morphism of G,H by A1;
    dom(F9) = G by Def14;
    hence thesis;
  end;
  redefine func cod(F) -> strict Element of V;
  coherence
  proof
    consider G,H being strict Element of V such that
A2: F is strict Morphism of G,H by Def25;
    reconsider F9 = F as Morphism of G,H by A2;
    cod(F9) = H by Def14;
    hence thesis;
  end;
end;

definition
  let V;
  let G be Element of V;
  func ID(G) -> strict Element of Morphs(V) equals
  ID(G);
  coherence
  proof
    reconsider G9 = G as strict Element of V by Def17;
    ID(G9) is strict Element of Morphs(V) by Def25;
    hence thesis;
  end;
end;

definition
  let V;
  func dom(V) -> Function of Morphs(V),V means
  :Def27:
  for f being Element of Morphs(V) holds it.f = dom(f);
  existence
  proof
    deffunc F(Element of Morphs(V)) = dom $1;
    consider F being Function of Morphs(V),V such that
A1: for f being Element of Morphs(V) holds F.f = F(f) from FUNCT_2:sch
    4;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F1,F2 be Function of Morphs(V),V such that
A2: for f being Element of Morphs(V) holds F1.f = dom(f) and
A3: for f being Element of Morphs(V) holds F2.f = dom(f);
    now
      let f be Element of Morphs(V);
      F1.f = dom(f) by A2;
      hence F1.f = F2.f by A3;
    end;
    hence thesis by FUNCT_2:63;
  end;
  func cod(V) -> Function of Morphs(V),V means
  :Def28:
  for f being Element of Morphs(V) holds it.f = cod(f);
  existence
  proof
    deffunc F(Element of Morphs(V)) = cod $1;
    consider F being Function of Morphs(V),V such that
A4: for f being Element of Morphs(V) holds F.f = F(f) from FUNCT_2:sch
    4;
    take F;
    thus thesis by A4;
  end;
  uniqueness
  proof
    let F1,F2 be Function of Morphs(V),V such that
A5: for f being Element of Morphs(V) holds F1.f = cod(f) and
A6: for f being Element of Morphs(V) holds F2.f = cod(f);
    now
      let f be Element of Morphs(V);
      F1.f = cod(f) by A5;
      hence F1.f = F2.f by A6;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

::
::  4d. Category of groups - superposition
::

theorem Th31:
  for g,f being Element of Morphs(V) st dom(g) = cod(f) ex G1,G2,
G3 being strict Element of V st g is Morphism of G2,G3 & f is Morphism of G1,G2
proof
  set X = Morphs(V);
  defpred P[Element of X,Element of X] means dom($1) = cod($2);
  let g,f be Element of X such that
A1: P[g,f];
  consider G2,G3 being strict Element of V such that
A2: g is strict Morphism of G2,G3 by Def25;
  consider G1,G29 being strict Element of V such that
A3: f is strict Morphism of G1,G29 by Def25;
A4: G29 = cod(f) by A3,Def14;
  G2 = dom(g) by A2,Def14;
  hence thesis by A1,A2,A3,A4;
end;

theorem Th32:
  for g,f being Element of Morphs(V) st dom(g) = cod(f) holds g*f in Morphs(V)
proof
  set X = Morphs(V);
  defpred P[Element of X,Element of X] means dom($1) = cod($2);
  let g,f be Element of X;
  assume P[g,f];
  then consider G1,G2,G3 being strict Element of V such that
A1: g is Morphism of G2,G3 and
A2: f is Morphism of G1,G2 by Th31;
  reconsider f9 = f as Morphism of G1,G2 by A2;
  reconsider g9 = g as Morphism of G2,G3 by A1;
  g9*f9 is Morphism of G1,G3;
  hence thesis by Def25;
end;

definition
  let V;
  func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means
  :Def30:
(for g,f being Element of Morphs(V) holds [g,f] in dom it iff dom(g) = cod(f))
  & for g,f being Element of Morphs(V) st [g,f] in dom it holds it.(g,f) = g*f;
  existence
  proof
    set X = Morphs(V);
    defpred P[Element of X,Element of X] means dom($1) = cod($2);
    deffunc F(Element of X,Element of X) = $1*$2;
A1: for g,f being Element of X st P[g,f] holds F(g,f) in X by Th32;
    consider c being PartFunc of [:X,X:],X such that
A2: ( for g,f being Element of X holds [g,f] in dom c iff P[g,f])& for
g,f being Element of X st [g,f] in dom c holds c.(g,f) = F(g,f) from BINOP_1:
    sch 8(A1);
    take c;
    thus thesis by A2;
  end;
  uniqueness
  proof
    set X = Morphs(V);
    defpred P[Element of X,Element of X] means dom($1) = cod($2);
    let c1,c2 be PartFunc of [:X,X:],X such that
A3: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and
A4: for g,f being Element of X st [g,f] in dom c1 holds c1.(g,f) = g*f and
A5: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and
A6: for g,f being Element of X st [g,f] in dom c2 holds c2.(g,f) = g*f;
    set V9 = dom c1;
A7: dom c1 c= [:X,X:] by RELAT_1:def 18;
    now
      let x;
      assume
A8:   x in dom c1;
      then consider g,f being Element of X such that
A9:   x = [g,f] by A7,SUBSET_1:43;
      P[g,f] by A3,A8,A9;
      hence x in dom c2 by A5,A9;
    end;
    then
A10: dom c1 c= dom c2 by TARSKI:def 3;
A11: for x,y st [x,y] in V9 holds c1.(x,y)=c2.(x,y)
    proof
      let x,y;
      assume
A12:  [x,y] in V9;
      then reconsider x,y as Element of X by A7,ZFMISC_1:87;
      c1.(x,y) = x*y by A4,A12;
      hence thesis by A6,A10,A12;
    end;
    now
      let x;
      assume
A13:  x in dom c2;
      dom c2 c= [:X,X:] by RELAT_1:def 18;
      then consider g,f being Element of X such that
A14:  x = [g,f] by A13,SUBSET_1:43;
      P[g,f] by A5,A13,A14;
      hence x in dom c1 by A3,A14;
    end;
    then dom c2 c= dom c1 by TARSKI:def 3;
    then dom c1 = dom c2 by A10,XBOOLE_0:def 10;
    hence thesis by A11,BINOP_1:20;
  end;
end;

::
::  4e. Definition of Category of groups
::

definition
  let UN;
  func GroupCat(UN) -> non empty non void strict CatStr equals
  CatStr(# GroupObjects(UN),Morphs(
    GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(
    GroupObjects(UN))#);
  coherence;
end;

registration
  let UN;
  cluster GroupCat(UN) -> strict non void non empty;
  coherence;
end;

theorem Th33:
  for f,g being Morphism of GroupCat(UN) holds [g,f] in dom(the
  Comp of GroupCat(UN)) iff dom g = cod f
proof
  set C = GroupCat(UN), V = GroupObjects(UN);
  let f,g be Morphism of C;
  reconsider f9 = f as Element of Morphs(V);
  reconsider g9 = g as Element of Morphs(V);
  dom g = dom(g9) & cod f = cod(f9) by Def27,Def28;
  hence thesis by Def30;
end;

theorem Th34:
  for f being (Morphism of GroupCat(UN)), f9 being Element of
  Morphs(GroupObjects(UN)), b being Object of GroupCat(UN), b9 being Element of
GroupObjects(UN) holds f is strict Element of Morphs(GroupObjects(UN)) & f9 is
  Morphism of GroupCat(UN) & b is strict Element of GroupObjects(UN) & b9 is
  Object of GroupCat(UN)
proof
  set C = GroupCat(UN), V = GroupObjects(UN);
  set X = Morphs(V);
  let f be (Morphism of C), f9 be Element of X, b be Object of C, b9 be
  Element of V;
  consider x such that
  x in UN and
A1: GO x,b by Def24;
  ex G,H being strict Element of V st f is strict Morphism of G,H by Def25;
  hence f is strict Element of X;
  thus f9 is Morphism of C;
  ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] & ex G being strict
AddGroup st b = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G &
  x4 = 0.G by A1,Def23;
  hence b is strict Element of V;
  thus thesis;
end;

canceled;

theorem Th36:
  for f,g being (Morphism of GroupCat(UN)),
      f9,g9 being Element of Morphs(GroupObjects(UN)) st f = f9 & g = g9
 holds
  (dom g = cod f iff dom g9 = cod f9) &
  (dom g = cod f iff [g9,f9] in dom comp(GroupObjects(UN))) &
  (dom g = cod f implies g(*)f = g9*f9) &
  (dom f = dom g iff dom f9 = dom g9) &
  (cod f = cod g iff cod f9 = cod g9)
proof
  set C = GroupCat(UN), V = GroupObjects(UN);
  set X = Morphs(V);
  let f,g be Morphism of C;
  let f9,g9 be Element of X;
  assume that
A1: f = f9 and
A2: g = g9;
A3: cod f = cod f9 by A1,Def28;
  hence dom g = cod f iff dom g9 = cod f9 by A2,Def27;
  dom g = dom g9 by A2,Def27;
  hence
A4: dom g = cod f iff [g9,f9] in dom comp(V) by A3,Def30;
  thus dom g = cod f implies g(*)f = g9*f9
  proof
    assume
A5: dom g = cod f;
    then [g,f] in dom (the Comp of C) by Th33;
    hence g(*)f = (comp(V)).(g9,f9) by A1,A2,CAT_1:def 1
      .= g9*f9 by A4,A5,Def30;
  end;
  dom f = dom f9 by A1,Def27;
  hence dom f = dom g iff dom f9 = dom g9 by A2,Def27;
  cod g = cod g9 by A2,Def28;
  hence thesis by A1,Def28;
end;

Lm1: for f,g being Morphism of GroupCat(UN) st dom g = cod f
 holds dom(g(*)f) = dom f & cod (g(*)f) = cod g
proof
  set X = Morphs(GroupObjects(UN));
  let f,g be Morphism of GroupCat(UN) such that
A1: dom g = cod f;
  reconsider g9 = g as strict Element of X by Th34;
  reconsider f9 = f as strict Element of X by Th34;
A2: dom g9 = cod f9 by A1,Th36;
  then reconsider gf = g9*f9 as Element of X by Th32;
A3: gf = g(*)f by A1,Th36;
  dom(g9*f9) = dom f9 & cod (g9*f9) = cod g9 by A2,Th20;
  hence thesis by A3,Th36;
end;

registration
  let UN;
  cluster GroupCat UN -> reflexive Category-like;
  coherence
  proof set C = GroupCat UN;
  thus C is reflexive
   proof let a be Element of C;
     reconsider G = a as Element of GroupObjects UN;
     consider x such that
   x in UN and
W2:   GO x,G by Def24;
     set ii = ID G;
     consider x1,x2,x3,x4 being set such that x = [x1,x2,x3,x4] and
W3:   ex H being strict AddGroup st G = H & x1 = the carrier of H &
         x2 = the addF of H & x3 = comp H & x4 = 0.H by W2,Def23;
     reconsider G as strict Element of GroupObjects UN by W3;
     reconsider ii as Morphism of C;
     reconsider ia = ii as GroupMorphismStr;
A:   dom ii = dom ia by Def27
       .= a;
     cod ii = cod ia by Def28
       .= a;
     then ii in Hom(a,a) by A;
    hence Hom(a,a)<>{};
   end;
  let f,g be Morphism of C;
    reconsider ff=f, gg=g as Element of Morphs GroupObjects UN;
   thus [g,f] in dom(the Comp of C) iff dom g = cod f by Th36;
  end;
end;

Lm3:
  for a being Element of GroupCat UN,
      aa being Element of GroupObjects UN st a = aa
   for i being Morphism of a,a st i = ID aa
    for b being Element of GroupCat UN holds
     (Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
     (Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
 proof
  let a be Element of GroupCat UN,
      aa be Element of GroupObjects UN such that
 a = aa;
  let i be Morphism of a,a such that
Z2: i = ID aa;
  let b be Element of GroupCat UN;
  thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
   proof assume
Z3:  Hom(a,b)<>{};
    let g be Morphism of a,b;
     reconsider gg=g, ii=i as Element of Morphs GroupObjects UN;
     consider G1,H1 being strict Element of GroupObjects UN such that
W1:   gg is strict Morphism of G1,H1 by Def25;
     consider f being Function of G1,H1 such that
W2:   gg = GroupMorphismStr(#G1,H1,f#) by W1,Th13;
D:   ii =  GroupMorphismStr(# aa,aa,id aa#) by Z2;
C:   cod ii = aa by Z2;
C2:  dom gg = G1 by W2;
E:   Hom(a,a) <> {};
     dom g = a by Z3,CAT_1:5 .= cod i by E,CAT_1:5;
     then
C1:   dom gg = cod ii by Th36;
     then aa =  dom gg by C;
     then
B:   aa = G1 by C2;
     then reconsider f as Function of aa,H1;
G1:  the GroupMorphismStr of gg = GroupMorphismStr(#aa,H1,f#) by W2,B;
A:   [gg,ii] in dom comp GroupObjects UN by Def30,C1;
     then [g,i] in dom the Comp of GroupCat UN;
    hence g(*)i = (the Comp of GroupCat UN).(g,i) by CAT_1:def 1
        .= (comp GroupObjects UN).(g,i)
        .= gg*ii by A,Def30
        .= GroupMorphismStr(# aa,H1,f*id aa#) by D,Def16,G1,C1
        .= GroupMorphismStr(# aa,H1,f#) by FUNCT_2:17
        .= g by B,W2;
   end;
  thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
   proof assume
Z3:  Hom(b,a)<>{};
    let g be Morphism of b,a;
     reconsider gg=g, ii=i as Element of Morphs GroupObjects UN;
     consider G1,H1 being strict Element of GroupObjects UN such that
W1:   gg is strict Morphism of G1,H1 by Def25;
     consider f being Function of G1,H1 such that
W2:   gg = GroupMorphismStr(#G1,H1,f#) by W1,Th13;
D:   ii =  GroupMorphismStr(# aa,aa,id aa#) by Z2;
C:   dom ii = aa by Z2;
C2:  cod gg = H1 by W2;
E:   Hom(a,a) <> {};
     cod g = a by Z3,CAT_1:5 .= dom i by E,CAT_1:5;
     then
C1:   cod gg = dom ii by Th36;
     then aa =  cod gg by C;
     then
B:   aa = H1 by C2;
     then reconsider f as Function of G1,aa;
G1:  the GroupMorphismStr of gg = GroupMorphismStr(#G1,aa,f#) by W2,B;
A:   [ii,gg] in dom comp GroupObjects UN by Def30,C1;
     then [i,g] in dom the Comp of GroupCat UN;
    hence i(*)g = (the Comp of GroupCat UN).(i,g) by CAT_1:def 1
        .= (comp GroupObjects UN).(i,g)
        .= ii*gg by A,Def30
        .= GroupMorphismStr(# G1,aa,(id aa)*f#) by D,Def16,G1,C1
        .= GroupMorphismStr(# G1,aa,f#) by FUNCT_2:17
        .= g by B,W2;
   end;
 end;

registration
  let UN;
  cluster GroupCat UN ->
   transitive associative with_identities;
  coherence
  proof set C = GroupCat UN;
   set X = Morphs(GroupObjects(UN));
   thus C is transitive
    proof
  let f,g be Morphism of GroupCat(UN) such that
A1: dom g = cod f;
  reconsider g9 = g as strict Element of X by Th34;
  reconsider f9 = f as strict Element of X by Th34;
A2: dom g9 = cod f9 by A1,Th36;
  then reconsider gf = g9*f9 as Element of X by Th32;
A3: gf = g(*)f by A1,Th36;
  dom(g9*f9) = dom f9 & cod (g9*f9) = cod g9 by A2,Th20;
  hence thesis by A3,Th36;
    end;
   thus C is associative
   proof
  let f,g,h be Morphism of (GroupCat(UN)) such that
A1: dom h = cod g & dom g = cod f;
  reconsider f9=f, g9=g, h9=h as strict Element of X by Th34;
A2: h9*g9 = h(*)g & dom(h(*)g) = cod(f) by A1,Lm1,Th36;
A3: dom h9 = cod g9 & dom g9 = cod f9 by A1,Th36;
  then reconsider gf = g9*f9, hg = h9*g9 as Element of X by Th32;
  g9*f9 = g(*)f & dom(h) = cod(g(*)f) by A1,Lm1,Th36;
  then h(*)(g(*)f) = h9*gf by Th36
    .= hg*f9 by A3,Th22
    .= (h(*)g)(*)f by A2,Th36;
  hence thesis;
  end;
  thus C is with_identities
   proof let a be Element of C;
     reconsider aa = a as Element of GroupObjects(UN);
    reconsider ii = ID aa as Morphism of C;
    reconsider ia = ii as GroupMorphismStr;
 A: dom ii = dom ia by Def27
       .= a;
    cod ii = cod ia by Def28
       .= a;
    then reconsider ii as Morphism of a,a by A,CAT_1:4;
    take ii;
    thus thesis by Lm3;
   end;
end;
end;

definition
  let UN;
  func AbGroupObjects(UN) -> Subset of the carrier of GroupCat(UN) equals
  {G
where G is Element of GroupCat(UN) : ex H being AbGroup st G = H
  };
  coherence
  proof
    set D2 = the carrier of GroupCat(UN);
    now
      let x be set;
      assume x in {G where G is Element of D2 : ex H being AbGroup st G = H};
      then ex G being Element of D2 st x = G & ex H being AbGroup st G = H;
      hence x in D2;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th37:
  Trivial-addLoopStr in AbGroupObjects(UN)
proof
  Trivial-addLoopStr in the carrier of GroupCat(UN) by Th29;
  hence thesis;
end;

registration
  let UN;
  cluster AbGroupObjects(UN) -> non empty;
  coherence by Th37;
end;

definition
  let UN;
  func AbGroupCat UN -> Subcategory of GroupCat(UN) equals
  cat AbGroupObjects UN;
  coherence;
end;

registration
  let UN;
  cluster AbGroupCat(UN) -> strict;
  coherence;
end;

theorem
  the carrier of AbGroupCat(UN) = AbGroupObjects(UN);

::  6. Subcategory of groups with the operator of 1/2

definition
  let UN;
  func MidOpGroupObjects(UN) -> Subset of the carrier of AbGroupCat(UN) equals
  {G where G is Element of AbGroupCat(UN) : ex H being
  midpoint_operator AbGroup st G = H};
  coherence
  proof
    set D2 = the carrier of AbGroupCat(UN);
    now
      let x be set;
      assume x in {G where G is Element of D2 : ex H being midpoint_operator
      AbGroup st G = H};
      then ex G being Element of D2 st x = G & ex H being midpoint_operator
      AbGroup st G = H;
      hence x in D2;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

registration
  let UN;
  cluster MidOpGroupObjects(UN) -> non empty;
  coherence
  proof
    set T = Trivial-addLoopStr;
    set D2 = the carrier of AbGroupCat(UN);
    set D1 = {G where G is Element of D2 : ex H being midpoint_operator
    AbGroup st G = H};
    T in D2 by Th37;
    then T in D1;
    then reconsider D1 as non empty set;
    now
      let x be set;
      assume x in D1;
      then ex G being Element of D2 st x = G & ex H being midpoint_operator
      AbGroup st G = H;
      hence x in D2;
    end;
    hence thesis;
  end;
end;

definition
  let UN;
  func MidOpGroupCat UN -> Subcategory of AbGroupCat(UN) equals
  cat MidOpGroupObjects UN;
  coherence;
end;

registration
  let UN;
  cluster MidOpGroupCat(UN) -> strict;
  coherence;
end;

theorem
  the carrier of MidOpGroupCat(UN) = MidOpGroupObjects(UN);

theorem
  Trivial-addLoopStr in MidOpGroupObjects(UN)
proof
  Trivial-addLoopStr in the carrier of AbGroupCat(UN) by Th37;
  hence thesis;
end;

theorem :: WAYBEL29:1
  for S, T being non empty 1-sorted for f being Function of S, T st f is
  one-to-one onto holds f*f" = id T & f"*f = id S & f" is one-to-one onto
proof
  let S, T be non empty 1-sorted;
  let f be Function of S, T;
A1: [#]T = the carrier of T;
  assume
A2: f is one-to-one onto;
  then
A3: rng f = the carrier of T by FUNCT_2:def 3;
  then dom f = the carrier of S & rng (f") = [#]S by A2,A1,FUNCT_2:def 1
,TOPS_2:49;
  hence thesis by A2,A3,A1,FUNCT_2:def 3,TOPS_2:50,52;
end;

theorem
  for a being Object of GroupCat(UN), aa being Element of
  GroupObjects(UN) st a = aa holds id a = ID aa
 proof let a be Object of GroupCat UN, aa be Element of GroupObjects UN;
  set C = GroupCat UN;
  assume
Z:  a = aa;
   reconsider ii = ID aa as Morphism of C;
   reconsider ia = ii as GroupMorphismStr;
A: dom ii = dom ia by Def27
      .= a by Z;
   cod ii = cod ia by Def28
      .= a by Z;
   then reconsider ii as Morphism of a,a by A,CAT_1:4;
  for b being Object of C holds
     (Hom(a,b) <> {} implies
       for f being Morphism of a,b holds f(*)ii = f)
   & (Hom(b,a) <> {} implies
     for f being Morphism of b,a holds ii(*)f = f) by Z,Lm3;
  hence id a = ID aa by CAT_1:def 12;              
 end;