:: GRCAT_1 semantic presentation

begin


theorem Th1: :: GRCAT_1:1
for UN being Universe
for u1, u2, u3, u4 being Element of UN holds
( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
proof
let UN be Universe; ::_thesis: for u1, u2, u3, u4 being Element of UN holds
( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
let u1, u2, u3, u4 be Element of UN; ::_thesis: ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
 ( [u1,u2,u3] = [[u1,u2],u3] & [u1,u2,u3,u4] = [[u1,u2,u3],u4] ) ;
hence  ( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN ) by CLASSES2:58; ::_thesis: verum
end;

theorem Th2: :: GRCAT_1:2
( op2 . ({},{}) = {} & op1 . {} = {} & op0 = {} )
proof
 [{},{}] in [:{{}},{{}}:] by ZFMISC_1:28;
hence  op2 . ({},{}) = {} by CARD_1:49, FUNCT_2:50; ::_thesis: ( op1 . {} = {} & op0 = {} )
 {} in {{}} by TARSKI:def_1;
hence  op1 . {} = {} by CARD_1:49, FUNCT_2:50; ::_thesis: op0 = {}
thus  op0 = {} ; ::_thesis: verum
end;

theorem Th3: :: GRCAT_1:3
for UN being Universe holds
( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
proof
let UN be Universe; ::_thesis: ( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
set D = {{}};
thus A1: {{}} in UN by CLASSES2:56, CLASSES2:57; ::_thesis: ( [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
hence  [{{}},{{}}] in UN by CLASSES2:58; ::_thesis: ( [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
A2: op2 in Funcs ([:{{}},{{}}:],{{}}) by CARD_1:49, FUNCT_2:8;
thus  [:{{}},{{}}:] in UN by A1, CLASSES2:61; ::_thesis: ( op2 in UN & op1 in UN )
then  Funcs ([:{{}},{{}}:],{{}}) in UN by A1, CLASSES2:61;
hence  op2 in UN by A2, ORDINAL1:10; ::_thesis: op1 in UN
A3: op1 in Funcs ({{}},{{}}) by CARD_1:49, FUNCT_2:8;
 Funcs ({{}},{{}}) in UN by A1, CLASSES2:61;
hence  op1 in UN by A3, ORDINAL1:10; ::_thesis: verum
end;

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

theorem :: GRCAT_1:4
( ( 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;


definition
let C be Category;
let O be non empty Subset of the carrier of C;
func Morphs O ->  Subset of the carrier' of C equals :: GRCAT_1:def 1
 union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
coherence
 union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  is Subset of the carrier' of C by CAT_2:19;
end;

:: deftheorem  defines Morphs GRCAT_1:def_1_:_
 for C being Category
for O being non empty Subset of the carrier of C holds Morphs O = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;

registration
let C be Category;
let O be non empty Subset of the carrier of C;
cluster Morphs O ->  non empty ;
coherence
 not Morphs O is empty by CAT_2:19;
end;

definition
let C be Category;
let O be non empty Subset of the carrier of C;
func dom O ->  Function of (Morphs O),O equals :: GRCAT_1:def 2
 the Source of C | (Morphs O);
coherence
 the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;
func cod O ->  Function of (Morphs O),O equals :: GRCAT_1:def 3
 the Target of C | (Morphs O);
coherence
 the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;
func comp O ->  PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) equals :: GRCAT_1:def 4
 the Comp of C || (Morphs O);
coherence
 the Comp of C || (Morphs O) is PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) by CAT_2:20;
canceled;
end;

:: deftheorem  defines dom GRCAT_1:def_2_:_
 for C being Category
for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O);

:: deftheorem  defines cod GRCAT_1:def_3_:_
 for C being Category
for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O);

:: deftheorem  defines comp GRCAT_1:def_4_:_
 for C being Category
for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O);

:: deftheorem  GRCAT_1:def_5_:_
canceled;

definition
let C be Category;
let O be non empty Subset of the carrier of C;
func cat O ->  Subcategory of C equals :: GRCAT_1:def 6
 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);
coherence
 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C
proof
 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is full Subcategory of C by CAT_2:21;
hence  CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C ; ::_thesis: verum
end;
end;

:: deftheorem  defines cat GRCAT_1:def_6_:_
 for C being Category
for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

registration
let C be Category;
let O be non empty Subset of the carrier of C;
cluster cat O ->  strict ;
coherence
 cat O is strict ;
end;

theorem :: GRCAT_1:5
for C being Category
for O being non empty Subset of the carrier of C holds the carrier of (cat O) = O ;

definition
let G be non empty 1-sorted ;
let H be non empty ZeroStr ;
func ZeroMap (G,H) ->  Function of G,H equals :: GRCAT_1:def 7
 the carrier of G --> (0. H);
coherence
 the carrier of G --> (0. H) is Function of G,H ;
end;

:: deftheorem  defines ZeroMap GRCAT_1:def_7_:_
 for G being non empty 1-sorted
for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H);

theorem Th6: :: GRCAT_1:6
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 ; ::_thesis: ( x in {{}} implies op1 . x = f . x )
assume  x in {{}} ; ::_thesis: op1 . x = f . x
then reconsider x = 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  op1 . x = f . x ; ::_thesis: verum
end;
hence  comp Trivial-addLoopStr = op1 by CARD_1:49, FUNCT_2:12; ::_thesis: verum
end;

registration
let G be non empty addMagma ;
let H be non empty right_zeroed addLoopStr ;
cluster ZeroMap (G,H) ->  additive ;
coherence
 ZeroMap (G,H) is additive
proof
set f = ZeroMap (G,H);
let x, y be Element of G; :: according to VECTSP_1:def_20 ::_thesis: (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y)
A1: (ZeroMap (G,H)) . y = 0. H by FUNCOP_1:7;
 ( (ZeroMap (G,H)) . (x + y) = 0. H & (ZeroMap (G,H)) . x = 0. H ) by FUNCOP_1:7;
hence  (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) by A1, RLVECT_1:def_4; ::_thesis: verum
end;
end;

registration
let G be non empty addMagma ;
let H be non empty right_zeroed addLoopStr ;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of G, the carrier of H:];
existence
 ex b1 being Function of G,H st b1 is additive
proof
take  ZeroMap (G,H) ; ::_thesis: ZeroMap (G,H) is additive
thus  ZeroMap (G,H) is additive ; ::_thesis: verum
end;
end;

theorem Th7: :: GRCAT_1:7
for G1, G2, G3 being non empty addMagma
for f being Function of G1,G2
for 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 ; ::_thesis: for f being Function of G1,G2
for g being Function of G2,G3 st f is additive & g is additive holds
g * f is additive
let f be Function of G1,G2; ::_thesis: for g being Function of G2,G3 st f is additive & g is additive holds
g * f is additive
let g be Function of G2,G3; ::_thesis: ( f is additive & g is additive implies g * f is additive )
assume that
A1: f is additive and
A2: g is additive ; ::_thesis: g * f is additive
set h = g * f;
now__::_thesis:_for_x,_y_being_Element_of_G1_holds_(g_*_f)_._(x_+_y)_=_((g_*_f)_._x)_+_((g_*_f)_._y)
let x, y be Element of G1; ::_thesis: (g * f) . (x + y) = ((g * f) . x) + ((g * f) . y)
A3: ( g . (f . x) = (g * f) . x & g . (f . y) = (g * f) . y ) by FUNCT_2:15;
thus (g * f) . (x + y) = g . (f . (x + y)) by FUNCT_2:15
.= g . ((f . x) + (f . y)) by A1, VECTSP_1:def_20
.= ((g * f) . x) + ((g * f) . y) by A2, A3, VECTSP_1:def_20 ; ::_thesis: verum
end;
hence  g * f is additive by VECTSP_1:def_20; ::_thesis: verum
end;

registration
let G1 be non empty addMagma ;
let G2, G3 be non empty right_zeroed addLoopStr ;
let f be additive Function of G1,G2;
let g be additive Function of G2,G3;
clusterf * g ->  additive for Function of G1,G3;
coherence
 for b1 being Function of G1,G3 st b1 = g * f holds
b1 is additive by Th7;
end;


definition
attrc1 is strict ;
struct GroupMorphismStr  -> ;
aggrGroupMorphismStr(# Source, Target, Fun #) ->  GroupMorphismStr ;
sel Source c1 ->  AddGroup;
sel Target c1 ->  AddGroup;
sel Fun c1 ->  Function of the Source of c1, the Target of c1;
end;

definition
canceled;
let f be GroupMorphismStr ;
func dom f ->  AddGroup equals :: GRCAT_1:def 9
 the Source of f;
coherence
 the Source of f is AddGroup ;
func cod f ->  AddGroup equals :: GRCAT_1:def 10
 the Target of f;
coherence
 the Target of f is AddGroup ;
end;

:: deftheorem  GRCAT_1:def_8_:_
canceled;

:: deftheorem  defines dom GRCAT_1:def_9_:_
 for f being GroupMorphismStr holds dom f = the Source of f;

:: deftheorem  defines cod GRCAT_1:def_10_:_
 for f being GroupMorphismStr holds cod f = the Target of f;

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

:: deftheorem  defines fun GRCAT_1:def_11_:_
 for f being GroupMorphismStr holds fun f = the Fun of f;

theorem :: GRCAT_1:8
for f being GroupMorphismStr
for G1, G2 being AddGroup
for 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 be AddGroup;
func ZERO (G,H) ->  GroupMorphismStr  equals :: GRCAT_1:def 12
 GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);
coherence
 GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ;
end;

:: deftheorem  defines ZERO GRCAT_1:def_12_:_
 for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

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

definition
let IT be GroupMorphismStr ;
attrIT is GroupMorphism-like  means :Def13: :: GRCAT_1:def 13
 fun IT is additive ;
end;

:: deftheorem Def13 defines GroupMorphism-like GRCAT_1:def_13_:_
 for IT being GroupMorphismStr holds
( IT is GroupMorphism-like iff fun IT is additive );

registration
cluster strict GroupMorphism-like for GroupMorphismStr ;
existence
 ex b1 being GroupMorphismStr st
( b1 is strict & b1 is GroupMorphism-like )
proof
set G = the AddGroup;
set z = ZERO ( the AddGroup, the AddGroup);
 fun (ZERO ( the AddGroup, the AddGroup)) is additive ;
then  ZERO ( the AddGroup, the AddGroup) is GroupMorphism-like by Def13;
hence  ex b1 being GroupMorphismStr st
( b1 is strict & b1 is GroupMorphism-like ) ; ::_thesis: verum
end;
end;

definition
mode GroupMorphism is GroupMorphism-like GroupMorphismStr ;
end;

theorem Th9: :: GRCAT_1:9
for F being GroupMorphism holds the Fun of F is additive
proof
let F be GroupMorphism; ::_thesis: the Fun of F is additive
 the Fun of F = fun F ;
hence  the Fun of F is additive by Def13; ::_thesis: verum
end;

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

definition
let G, H be AddGroup;
mode Morphism of G,H ->  GroupMorphism means :Def14: :: GRCAT_1:def 14
( dom it = G & cod it = H );
existence
 ex b1 being GroupMorphism st
( dom b1 = G & cod b1 = H )
proof
take  ZERO (G,H) ; ::_thesis: ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H )
thus  ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines Morphism GRCAT_1:def_14_:_
 for G, H being AddGroup
for b3 being GroupMorphism holds
( b3 is Morphism of G,H iff ( dom b3 = G & cod b3 = H ) );

registration
let G, H be AddGroup;
cluster strict GroupMorphism-like for Morphism of G,H;
existence
 ex b1 being Morphism of G,H st b1 is strict
proof
 ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ;
then  ZERO (G,H) is Morphism of G,H by Def14;
hence  ex b1 being Morphism of G,H st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th10: :: GRCAT_1:10
for G, H being AddGroup
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 G, H be AddGroup; ::_thesis: for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds
f is strict Morphism of G,H
let f be strict GroupMorphismStr ; ::_thesis: ( dom f = G & cod f = H & fun f is additive implies f is strict Morphism of G,H )
assume that
A1: ( dom f = G & cod f = H ) and
A2: fun f is additive ; ::_thesis: f is strict Morphism of G,H
reconsider f9 = f as strict GroupMorphism by A2, Def13;
 f9 is strict Morphism of G,H by A1, Def14;
hence  f is strict Morphism of G,H ; ::_thesis: verum
end;

theorem Th11: :: GRCAT_1:11
for G, H being AddGroup
for f being Function of G,H st f is additive holds
GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
proof
let G, H be AddGroup; ::_thesis: for f being Function of G,H st f is additive holds
GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
let f be Function of G,H; ::_thesis: ( f is additive implies GroupMorphismStr(# G,H,f #) is strict Morphism of G,H )
assume A1: f is additive ; ::_thesis: GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
set F = GroupMorphismStr(# G,H,f #);
 fun GroupMorphismStr(# G,H,f #) = f ;
hence  GroupMorphismStr(# G,H,f #) is strict Morphism of G,H by A1, Th10; ::_thesis: verum
end;

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

definition
let G be AddGroup;
func ID G ->  Morphism of G,G equals :: GRCAT_1:def 15
 GroupMorphismStr(# G,G,(id G) #);
coherence
 GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G
proof
set i = GroupMorphismStr(# G,G,(id G) #);
 fun GroupMorphismStr(# G,G,(id G) #) = id G ;
hence  GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G by Th10; ::_thesis: verum
end;
end;

:: deftheorem  defines ID GRCAT_1:def_15_:_
 for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #);

registration
let G be AddGroup;
cluster ID G ->  strict ;
coherence
 ID G is strict ;
end;

definition
let G, H be AddGroup;
:: original: ZERO
redefine func ZERO (G,H) ->  strict Morphism of G,H;
coherence
 ZERO (G,H) is strict Morphism of G,H
proof
set i = ZERO (G,H);
 fun (ZERO (G,H)) = ZeroMap (G,H) ;
hence  ZERO (G,H) is strict Morphism of G,H by Th10; ::_thesis: verum
end;
end;

theorem Th12: :: GRCAT_1:12
for G, H being AddGroup
for F being Morphism of G,H ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
proof
let G, H be AddGroup; ::_thesis: for F being Morphism of G,H ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
let F be Morphism of G,H; ::_thesis: ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
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 ; ::_thesis: ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
thus  ( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive ) by A2, A1, Th9; ::_thesis: verum
end;

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

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

theorem :: GRCAT_1:15
for F being strict GroupMorphism ex G, H being AddGroup ex 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; ::_thesis: ex G, H being AddGroup ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
consider G, H being AddGroup 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 ; ::_thesis: ex H being AddGroup ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
take  H ; ::_thesis: ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
take  f ; ::_thesis: ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
thus  ( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive ) by A2; ::_thesis: verum
end;

theorem Th16: :: GRCAT_1:16
for g, f being GroupMorphism st dom g = cod f holds
ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof
defpred S1[ GroupMorphism, GroupMorphism] means  dom $1 = cod $2;
let g, f be GroupMorphism; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
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  ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum
end;

definition
let G, F be GroupMorphism;
assume A1: dom G = cod F ;
funcG * F ->  strict GroupMorphism means :Def16: :: GRCAT_1:def 16
 for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
it = GroupMorphismStr(# G1,G3,(g * f) #);
existence
 ex b1 being strict GroupMorphism st
for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b1 = GroupMorphismStr(# G1,G3,(g * f) #)
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: GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G19,G29,f9 #) and
A5: f9 is additive by A3, Th12;
consider g9 being Function of G29,G39 such that
A6: GroupMorphismStr(# the Source of G, the Target of G, the Fun 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 ; ::_thesis: for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
T9 = GroupMorphismStr(# G1,G3,(g * f) #)
thus  for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
T9 = GroupMorphismStr(# G1,G3,(g * f) #) by A6, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict GroupMorphism st ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b2 = GroupMorphismStr(# G1,G3,(g * f) #) ) holds
b1 = b2
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 = F9 as Morphism of G19,G29 by A1, Def14;
consider f9 being Function of G19,G29 such that
A10: GroupMorphismStr(# the Source of F9, the Target of F9, the Fun 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; ::_thesis: ( ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
S1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
S2 = GroupMorphismStr(# G1,G3,(g * f) #) ) implies S1 = S2 )
assume that
A11: for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
S1 = GroupMorphismStr(# G1,G3,(g * f) #) and
A12: for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
S2 = GroupMorphismStr(# G1,G3,(g * f) #) ; ::_thesis: S1 = S2
consider g9 being Function of G29,G39 such that
A13: GroupMorphismStr(# the Source of G9, the Target of G9, the Fun 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 ; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines * GRCAT_1:def_16_:_
 for G, F being GroupMorphism st dom G = cod F holds
for b3 being strict GroupMorphism holds
( b3 = G * F iff for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b3 = GroupMorphismStr(# G1,G3,(g * f) #) );

theorem Th17: :: GRCAT_1:17
for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
proof
let G1, G2, G3 be AddGroup; ::_thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
let F be Morphism of G1,G2; ::_thesis: G * F is Morphism of G1,G3
consider g being Function of G2,G3 such that
A1: GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) and
 g is additive by Th12;
consider f being Function of G1,G2 such that
A2: GroupMorphismStr(# the Source of F, the Target of F, the Fun 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  G * F is Morphism of G1,G3 by Def14; ::_thesis: verum
end;

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

theorem Th18: :: GRCAT_1:18
for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for 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; ::_thesis: for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for 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) #)
let G be Morphism of G2,G3; ::_thesis: for F being Morphism of G1,G2
for g being Function of G2,G3
for 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) #)
let F be Morphism of G1,G2; ::_thesis: for g being Function of G2,G3
for 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) #)
let g be Function of G2,G3; ::_thesis: for 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) #)
let f be Function of G1,G2; ::_thesis: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) implies G * F = GroupMorphismStr(# G1,G3,(g * f) #) )
assume A1: ( G = GroupMorphismStr(# G2,G3,g #) & F = GroupMorphismStr(# G1,G2,f #) ) ; ::_thesis: G * F = GroupMorphismStr(# G1,G3,(g * f) #)
dom G = G2 by Def14
.= cod F by Def14 ;
hence  G * F = GroupMorphismStr(# G1,G3,(g * f) #) by A1, Def16; ::_thesis: verum
end;

theorem Th19: :: GRCAT_1:19
for f, g being strict GroupMorphism st dom g = cod f holds
ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex 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; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) ) )
assume A1: dom g = cod f ; ::_thesis: ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) )
set G1 = dom f;
set G2 = cod f;
set G3 = cod g;
reconsider f9 = f as strict Morphism of dom f, cod f by Def14;
reconsider g9 = g as strict Morphism of cod f, cod g by A1, Def14;
consider f0 being Function of (dom f),(cod f) such that
A2: f9 = GroupMorphismStr(# (dom f),(cod f),f0 #) ;
consider g0 being Function of (cod f),(cod g) such that
A3: g9 = GroupMorphismStr(# (cod f),(cod g),g0 #) by Th13;
take  dom f ; ::_thesis: ex G2, G3 being AddGroup ex f0 being Function of (dom f),G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# (dom f),G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod f ; ::_thesis: ex G3 being AddGroup ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),G3 st
( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),G3,g0 #) & g * f = GroupMorphismStr(# (dom f),G3,(g0 * f0) #) )
take  cod g ; ::_thesis: ex f0 being Function of (dom f),(cod f) ex g0 being Function of (cod f),(cod g) st
( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  f0 ; ::_thesis: ex g0 being Function of (cod f),(cod g) st
( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
take  g0 ; ::_thesis: ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) )
thus  ( f = GroupMorphismStr(# (dom f),(cod f),f0 #) & g = GroupMorphismStr(# (cod f),(cod g),g0 #) & g * f = GroupMorphismStr(# (dom f),(cod g),(g0 * f0) #) ) by A2, A3, Th18; ::_thesis: verum
end;

theorem Th20: :: GRCAT_1:20
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; ::_thesis: ( dom g = cod f implies ( dom (g * f) = dom f & cod (g * f) = cod g ) )
assume  dom g = cod f ; ::_thesis: ( dom (g * f) = dom f & cod (g * f) = cod g )
then A1: ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex 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 ; ::_thesis: cod (g * f) = cod g
thus  cod (g * f) = cod g by A1; ::_thesis: verum
end;

theorem Th21: :: GRCAT_1:21
for G1, G2, G3, G4 being AddGroup
for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
proof
let G1, G2, G3, G4 be AddGroup; ::_thesis: for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let f be strict Morphism of G1,G2; ::_thesis: for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let g be strict Morphism of G2,G3; ::_thesis: for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
let h be strict Morphism of G3,G4; ::_thesis: h * (g * f) = (h * g) * f
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  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem Th22: :: GRCAT_1:22
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; ::_thesis: ( dom h = cod g & dom g = cod f implies h * (g * f) = (h * g) * f )
assume that
A1: dom h = cod g and
A2: dom g = cod f ; ::_thesis: h * (g * f) = (h * g) * f
set G2 = cod f;
set G3 = cod g;
reconsider h9 = h as Morphism of cod g, cod h by A1, Def14;
reconsider g9 = g as Morphism of cod f, cod g by A2, Def14;
reconsider f9 = f as Morphism of dom f, cod f by Def14;
 h9 * (g9 * f9) = (h9 * g9) * f9 by Th21;
hence  h * (g * f) = (h * g) * f ; ::_thesis: verum
end;

theorem :: GRCAT_1:23
for G being AddGroup holds
( 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
let G be AddGroup; ::_thesis: ( 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 ) )
set i = ID G;
thus  dom (ID G) = G ; ::_thesis: ( 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 ) )
thus  cod (ID G) = G ; ::_thesis: ( ( 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 ) )
thus  for f being strict GroupMorphism st cod f = G holds
(ID G) * f = f ::_thesis: for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g
proof
let f be strict GroupMorphism; ::_thesis: ( cod f = G implies (ID G) * f = f )
assume A1: cod f = G ; ::_thesis: (ID G) * f = f
set H = dom f;
reconsider f9 = f as Morphism of dom f,G by A1, Def14;
consider m being Function of (dom f),G such that
A2: f9 = GroupMorphismStr(# (dom f),G,m #) by Th13;
 ( dom (ID G) = G & (id G) * m = m ) by FUNCT_2:17;
hence  (ID G) * f = f by A1, A2, Def16; ::_thesis: verum
end;
thus  for g being strict GroupMorphism st dom g = G holds
g * (ID G) = g ::_thesis: verum
proof
let f be strict GroupMorphism; ::_thesis: ( dom f = G implies f * (ID G) = f )
assume A3: dom f = G ; ::_thesis: f * (ID G) = f
set H = cod f;
reconsider f9 = f as Morphism of G, cod f by A3, Def14;
consider m being Function of G,(cod f) such that
A4: f9 = GroupMorphismStr(# G,(cod f),m #) by Th13;
 ( cod (ID G) = G & m * (id G) = m ) by FUNCT_2:17;
hence  f * (ID G) = f by A3, A4, Def16; ::_thesis: verum
end;
end;

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

:: deftheorem Def17 defines Group_DOMAIN-like GRCAT_1:def_17_:_
 for IT being set holds
( IT is Group_DOMAIN-like iff for x being set st x in IT holds
x is strict AddGroup );

registration
cluster non empty Group_DOMAIN-like for set ;
existence
 ex b1 being set st
( b1 is Group_DOMAIN-like & not b1 is empty )
proof
set D = {Trivial-addLoopStr};
take  {Trivial-addLoopStr} ; ::_thesis: ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty )
 for x being set st x in {Trivial-addLoopStr} holds
x is strict AddGroup by TARSKI:def_1;
hence  ( {Trivial-addLoopStr} is Group_DOMAIN-like & not {Trivial-addLoopStr} is empty ) by Def17; ::_thesis: verum
end;
end;

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

definition
let V be Group_DOMAIN;
:: original: Element
redefine mode Element of V ->  AddGroup;
coherence
 for b1 being Element of V holds b1 is AddGroup by Def17;
end;

registration
let V be Group_DOMAIN;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for Element of V;
existence
 ex b1 being Element of V st b1 is strict
proof
set v = the Element of V;
 the Element of V is strict AddGroup by Def17;
hence  ex b1 being Element of V st b1 is strict ; ::_thesis: verum
end;
end;

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

:: deftheorem Def18 defines GroupMorphism_DOMAIN-like GRCAT_1:def_18_:_
 for IT being set holds
( IT is GroupMorphism_DOMAIN-like iff for x being set st x in IT holds
x is strict GroupMorphism );

registration
cluster non empty GroupMorphism_DOMAIN-like for set ;
existence
 ex b1 being set st
( b1 is GroupMorphism_DOMAIN-like & not b1 is empty )
proof
set G = the AddGroup;
take  {(ID the AddGroup)} ; ::_thesis: ( {(ID the AddGroup)} is GroupMorphism_DOMAIN-like & not {(ID the AddGroup)} is empty )
 for x being set st x in {(ID the AddGroup)} holds
x is strict GroupMorphism by TARSKI:def_1;
hence  ( {(ID the AddGroup)} is GroupMorphism_DOMAIN-like & not {(ID the AddGroup)} is empty ) by Def18; ::_thesis: verum
end;
end;

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

definition
let M be GroupMorphism_DOMAIN;
:: original: Element
redefine mode Element of M ->  GroupMorphism;
coherence
 for b1 being Element of M holds b1 is GroupMorphism by Def18;
end;

registration
let M be GroupMorphism_DOMAIN;
cluster strict GroupMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proof
set m = the Element of M;
 the Element of M is strict GroupMorphism by Def18;
hence  ex b1 being Element of M st b1 is strict ; ::_thesis: verum
end;
end;

theorem Th24: :: GRCAT_1:24
for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
proof
let f be strict GroupMorphism; ::_thesis: {f} is GroupMorphism_DOMAIN
 for x being set st x in {f} holds
x is strict GroupMorphism by TARSKI:def_1;
hence  {f} is GroupMorphism_DOMAIN by Def18; ::_thesis: verum
end;

definition
let G, H be AddGroup;
mode GroupMorphism_DOMAIN of G,H ->  GroupMorphism_DOMAIN means :Def19: :: GRCAT_1:def 19
 for x being Element of it holds x is strict Morphism of G,H;
existence
 ex b1 being GroupMorphism_DOMAIN st
for x being Element of b1 holds x is strict Morphism of G,H
proof
reconsider D = {(ZERO (G,H))} as GroupMorphism_DOMAIN by Th24;
take  D ; ::_thesis: for x being Element of D holds x is strict Morphism of G,H
thus  for x being Element of D holds x is strict Morphism of G,H by TARSKI:def_1; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines GroupMorphism_DOMAIN GRCAT_1:def_19_:_
 for G, H being AddGroup
for b3 being GroupMorphism_DOMAIN holds
( b3 is GroupMorphism_DOMAIN of G,H iff for x being Element of b3 holds x is strict Morphism of G,H );

theorem Th25: :: GRCAT_1:25
for D being non empty set
for G, H being AddGroup holds
( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
proof
let D be non empty set ; ::_thesis: for G, H being AddGroup holds
( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
let G, H be AddGroup; ::_thesis: ( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
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; ::_thesis: ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is GroupMorphism_DOMAIN of G,H )
thus  ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is GroupMorphism_DOMAIN of G,H ) ::_thesis: verum
proof
assume A1: for x being Element of D holds x is strict Morphism of G,H ; ::_thesis: D is GroupMorphism_DOMAIN 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  D is GroupMorphism_DOMAIN of G,H by Def19; ::_thesis: verum
end;
end;

theorem :: GRCAT_1:26
for G, H being AddGroup
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H
proof
let G, H be AddGroup; ::_thesis: for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H
let f be strict Morphism of G,H; ::_thesis: {f} is GroupMorphism_DOMAIN of G,H
 for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def_1;
hence  {f} is GroupMorphism_DOMAIN of G,H by Th25; ::_thesis: verum
end;

definition
let G, H be 1-sorted ;
mode MapsSet of G,H ->  set  means :Def20: :: GRCAT_1:def 20
 for x being set st x in it holds
x is Function of G,H;
existence
 ex b1 being set st
for x being set st x in b1 holds
x is Function of G,H
proof
take  {} ; ::_thesis: for x being set st x in {} holds
x is Function of G,H
thus  for x being set st x in {} holds
x is Function of G,H ; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines MapsSet GRCAT_1:def_20_:_
 for G, H being 1-sorted
for b3 being set holds
( b3 is MapsSet of G,H iff for x being set st x in b3 holds
x is Function of G,H );

definition
let G, H be 1-sorted ;
func Maps (G,H) ->  MapsSet of G,H equals :: GRCAT_1:def 21
 Funcs ( the carrier of G, the carrier of H);
coherence
 Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H
proof
let x be set ; :: according to GRCAT_1:def_20 ::_thesis: ( x in Funcs ( the carrier of G, the carrier of H) implies x is Function of G,H )
assume  x in Funcs ( the carrier of G, the carrier of H) ; ::_thesis: x is Function of G,H
hence  x is Function of G,H by FUNCT_2:66; ::_thesis: verum
end;
end;

:: deftheorem  defines Maps GRCAT_1:def_21_:_
 for G, H being 1-sorted holds Maps (G,H) = Funcs ( the carrier of G, the carrier of H);

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

registration
let G be 1-sorted ;
let H be non empty 1-sorted ;
cluster non empty for MapsSet of G,H;
existence
 not for b1 being MapsSet of G,H holds b1 is empty
proof
 not Maps (G,H) is empty ;
hence  not for b1 being MapsSet of G,H holds b1 is empty ; ::_thesis: verum
end;
end;

definition
let G be 1-sorted ;
let H be non empty 1-sorted ;
let M be non empty MapsSet of G,H;
:: original: Element
redefine mode Element of M ->  Function of G,H;
coherence
 for b1 being Element of M holds b1 is Function of G,H by Def20;
end;

definition
let G, H be AddGroup;
func Morphs (G,H) ->  GroupMorphism_DOMAIN of G,H means :Def22: :: GRCAT_1:def 22
 for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
 ex b1 being GroupMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
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  {  GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive  }  ;
then reconsider D =  {  GroupMorphismStr(# G,H,f #) where f is Element of Maps (G,H) : f is additive  }  as non empty set ;
A1: for x being set st x in D holds
x is strict Morphism of G,H
proof
let x be set ; ::_thesis: ( x in D implies x is strict Morphism of G,H )
assume  x in D ; ::_thesis: x is strict Morphism of G,H
then  ex f being Element of Maps (G,H) st
( x = GroupMorphismStr(# G,H,f #) & f is additive ) ;
hence  x is strict Morphism of G,H by Th11; ::_thesis: verum
end;
then A2: for x being Element of D holds x is strict Morphism of G,H ;
A3: for x being set st x is strict Morphism of G,H holds
x in D
proof
let x be set ; ::_thesis: ( x is strict Morphism of G,H implies x in D )
assume  x is strict Morphism of G,H ; ::_thesis: x in D
then reconsider x = 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  x in D by A5; ::_thesis: verum
end;
reconsider D = D as GroupMorphism_DOMAIN of G,H by A2, Th25;
take  D ; ::_thesis: for x being set holds
( x in D iff x is strict Morphism of G,H )
thus  for x being set holds
( x in D iff x is strict Morphism of G,H ) by A1, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being GroupMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
proof
let D1, D2 be GroupMorphism_DOMAIN of G,H; ::_thesis: ( ( for x being set holds
( x in D1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in D2 iff x is strict Morphism of G,H ) ) implies D1 = D2 )
assume that
A6: for x being set holds
( x in D1 iff x is strict Morphism of G,H ) and
A7: for x being set holds
( x in D2 iff x is strict Morphism of G,H ) ; ::_thesis: D1 = D2
 for x being set holds
( x in D1 iff x in D2 )
proof
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
thus  ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 )
proof
assume  x in D1 ; ::_thesis: x in D2
then  x is strict Morphism of G,H by A6;
hence  x in D2 by A7; ::_thesis: verum
end;
thus  ( x in D2 implies x in D1 ) ::_thesis: verum
proof
assume  x in D2 ; ::_thesis: x in D1
then  x is strict Morphism of G,H by A7;
hence  x in D1 by A6; ::_thesis: verum
end;
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines Morphs GRCAT_1:def_22_:_
 for G, H being AddGroup
for b3 being GroupMorphism_DOMAIN of G,H holds
( b3 = Morphs (G,H) iff for x being set holds
( x in b3 iff x is strict Morphism of G,H ) );

definition
let G, H be AddGroup;
let M be GroupMorphism_DOMAIN of G,H;
:: original: Element
redefine mode Element of M ->  Morphism of G,H;
coherence
 for b1 being Element of M holds b1 is Morphism of G,H by Def19;
end;

registration
let G, H be AddGroup;
let M be GroupMorphism_DOMAIN of G,H;
cluster strict GroupMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proof
set m = the Element of M;
 the Element of M is strict Morphism of G,H by Def19;
hence  ex b1 being Element of M st b1 is strict ; ::_thesis: verum
end;
end;

definition
let x, y be set ;
pred GO x,y means :Def23: :: GRCAT_1:def 23
 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;

:: deftheorem Def23 defines GO GRCAT_1:def_23_:_
 for x, y being set holds
( GO x,y iff 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 ) ) );

theorem Th27: :: GRCAT_1:27
for x, y1, y2 being set st GO x,y1 & GO x,y2 holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( GO x,y1 & GO x,y2 implies y1 = y2 )
assume that
A1: GO x,y1 and
A2: GO x,y2 ; ::_thesis: y1 = 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  y1 = y2 by A3, A8, A5, A7, A10, A12, XTUPLE_0:5; ::_thesis: verum
end;

theorem Th28: :: GRCAT_1:28
for UN being Universe ex x being set st
( x in UN & GO x, Trivial-addLoopStr )
proof
let UN be Universe; ::_thesis: ex x being set st
( x in UN & GO x, Trivial-addLoopStr )
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 = [{u},x2,x3,x4]; ::_thesis: ( x in UN & GO x, Trivial-addLoopStr )
thus  x in UN by Th1; ::_thesis: GO x, Trivial-addLoopStr
take  {u} ; :: according to GRCAT_1:def_23 ::_thesis: ex x2, x3, x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take  x2 ; ::_thesis: ex x3, x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take  x3 ; ::_thesis: ex x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take  x4 ; ::_thesis: ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
thus  x = [{u},x2,x3,x4] ; ::_thesis: ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G )
take  Trivial-addLoopStr ; ::_thesis: ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr )
thus  ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr ) by CARD_1:49; ::_thesis: verum
end;

definition
let UN be Universe;
func GroupObjects UN ->  set  means :Def24: :: GRCAT_1:def 24
 for y being set holds
( y in it iff ex x being set st
( x in UN & GO x,y ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) )
proof
defpred S1[ set , set ] means  GO $1,$2;
A1: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by Th27;
consider Y being set  such that
A2: for y being set holds
( y in Y iff ex x being set st
( x in UN & S1[x,y] ) ) from TARSKI:sch_1(A1);
take  Y ; ::_thesis: for y being set holds
( y in Y iff ex x being set st
( x in UN & GO x,y ) )
thus  for y being set holds
( y in Y iff ex x being set st
( x in UN & GO x,y ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex x being set st
( x in UN & GO x,$1 );
 for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3();
hence  for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) ) holds
b1 = b2 ; ::_thesis: verum
end;
end;

:: deftheorem Def24 defines GroupObjects GRCAT_1:def_24_:_
 for UN being Universe
for b2 being set holds
( b2 = GroupObjects UN iff for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) );

theorem Th29: :: GRCAT_1:29
for UN being Universe holds Trivial-addLoopStr in GroupObjects UN
proof
let UN be Universe; ::_thesis: Trivial-addLoopStr in GroupObjects UN
 ex x being set st
( x in UN & GO x, Trivial-addLoopStr ) by Th28;
hence  Trivial-addLoopStr in GroupObjects UN by Def24; ::_thesis: verum
end;

registration
let UN be Universe;
cluster GroupObjects UN ->  non empty ;
coherence
 not GroupObjects UN is empty by Th29;
end;

theorem Th30: :: GRCAT_1:30
for UN being Universe
for x being Element of GroupObjects UN holds x is strict AddGroup
proof
let UN be Universe; ::_thesis: for x being Element of GroupObjects UN holds x is strict AddGroup
let x be Element of GroupObjects UN; ::_thesis: x is strict AddGroup
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  x is strict AddGroup ; ::_thesis: verum
end;

registration
let UN be Universe;
cluster GroupObjects UN ->  Group_DOMAIN-like ;
coherence
 GroupObjects UN is Group_DOMAIN-like
proof
let x be set ; :: according to GRCAT_1:def_17 ::_thesis: ( x in GroupObjects UN implies x is strict AddGroup )
thus  ( x in GroupObjects UN implies x is strict AddGroup ) by Th30; ::_thesis: verum
end;
end;

definition
let V be Group_DOMAIN;
func Morphs V ->  GroupMorphism_DOMAIN means :Def25: :: GRCAT_1:def 25
 for x being set holds
( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H );
existence
 ex b1 being GroupMorphism_DOMAIN st
for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proof
set G0 = the strict Element of V;
set M = Morphs ( the strict Element of V, the strict Element of V);
set S =  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ;
 ( ZERO ( the strict Element of V, the strict Element of V) is Element of Morphs ( the strict Element of V, the strict Element of V) & Morphs ( the strict Element of V, the strict Element of V) in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ) by Def22;
then reconsider T = union  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  as non empty set by TARSKI:def_4;
A1: for x being set holds
( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proof
let x be set ; ::_thesis: ( x in T iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus  ( x in T implies ex G, H being strict Element of V st x is strict Morphism of G,H ) ::_thesis: ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T )
proof
assume  x in T ; ::_thesis: ex G, H being strict Element of V st x is strict Morphism of G,H
then consider Y being set  such that
A2: x in Y and
A3: Y in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  by TARSKI:def_4;
consider G, H being strict Element of V such that
A4: Y = Morphs (G,H) by A3;
take  G ; ::_thesis: ex H being strict Element of V st x is strict Morphism of G,H
take  H ; ::_thesis: x is strict Morphism of G,H
thus  x is strict Morphism of G,H by A2, A4, Def22; ::_thesis: verum
end;
thus  ( ex G, H being strict Element of V st x is strict Morphism of G,H implies x in T ) ::_thesis: verum
proof
given G, H being strict Element of V such that A5: x is strict Morphism of G,H ; ::_thesis: x in T
set M = Morphs (G,H);
A6: Morphs (G,H) in  {  (Morphs (G,H)) where G, H is strict Element of V : verum  }  ;
 x in Morphs (G,H) by A5, Def22;
hence  x in T by A6, TARSKI:def_4; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_set_st_x_in_T_holds_
x_is_strict_GroupMorphism
let x be set ; ::_thesis: ( x in T implies x is strict GroupMorphism )
assume  x in T ; ::_thesis: x is strict GroupMorphism
then  ex G, H being strict Element of V st x is strict Morphism of G,H by A1;
hence  x is strict GroupMorphism ; ::_thesis: verum
end;
then reconsider T9 = T as GroupMorphism_DOMAIN by Def18;
take  T9 ; ::_thesis: for x being set holds
( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
thus  for x being set holds
( x in T9 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being GroupMorphism_DOMAIN st ( for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b1 = b2
proof
let D1, D2 be GroupMorphism_DOMAIN; ::_thesis: ( ( for x being set holds
( x in D1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) implies D1 = D2 )
assume that
A7: for x being set 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 being set holds
( x in D2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_x_in_D1_iff_x_in_D2_)
let x be set ; ::_thesis: ( x in D1 iff x in D2 )
 ( 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; ::_thesis: verum
end;
hence  D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def25 defines Morphs GRCAT_1:def_25_:_
 for V being Group_DOMAIN
for b2 being GroupMorphism_DOMAIN holds
( b2 = Morphs V iff for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

definition
let V be Group_DOMAIN;
let F be Element of Morphs V;
:: original: dom
redefine func dom F ->  strict Element of V;
coherence
 dom F is strict Element of V
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  dom F is strict Element of V ; ::_thesis: verum
end;
:: original: cod
redefine func cod F ->  strict Element of V;
coherence
 cod F is strict Element of V
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  cod F is strict Element of V ; ::_thesis: verum
end;
end;

definition
let V be Group_DOMAIN;
let G be Element of V;
func ID G ->  strict Element of Morphs V equals :: GRCAT_1:def 26
 ID G;
coherence
 ID G is strict Element of Morphs V
proof
reconsider G9 = G as strict Element of V by Def17;
 ID G9 is strict Element of Morphs V by Def25;
hence  ID G is strict Element of Morphs V ; ::_thesis: verum
end;
end;

:: deftheorem  defines ID GRCAT_1:def_26_:_
 for V being Group_DOMAIN
for G being Element of V holds ID G = ID G;

definition
let V be Group_DOMAIN;
func dom V ->  Function of (Morphs V),V means :Def27: :: GRCAT_1:def 27
 for f being Element of Morphs V holds it . f = dom f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom f
proof
deffunc H1( Element of Morphs V) ->  strict Element of V = dom $1;
consider F being Function of (Morphs V),V such that
A1: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = dom f
thus  for f being Element of Morphs V holds F . f = dom f by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom f ) & ( for f being Element of Morphs V holds b2 . f = dom f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = dom f ) & ( for f being Element of Morphs V holds F2 . f = dom f ) implies F1 = F2 )
assume 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 ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = dom f by A2;
hence  F1 . f = F2 . f by A3; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
func cod V ->  Function of (Morphs V),V means :Def28: :: GRCAT_1:def 28
 for f being Element of Morphs V holds it . f = cod f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod f
proof
deffunc H1( Element of Morphs V) ->  strict Element of V = cod $1;
consider F being Function of (Morphs V),V such that
A4: for f being Element of Morphs V holds F . f = H1(f) from FUNCT_2:sch_4();
take  F ; ::_thesis: for f being Element of Morphs V holds F . f = cod f
thus  for f being Element of Morphs V holds F . f = cod f by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod f ) & ( for f being Element of Morphs V holds b2 . f = cod f ) holds
b1 = b2
proof
let F1, F2 be Function of (Morphs V),V; ::_thesis: ( ( for f being Element of Morphs V holds F1 . f = cod f ) & ( for f being Element of Morphs V holds F2 . f = cod f ) implies F1 = F2 )
assume 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 ; ::_thesis: F1 = F2
now__::_thesis:_for_f_being_Element_of_Morphs_V_holds_F1_._f_=_F2_._f
let f be Element of Morphs V; ::_thesis: F1 . f = F2 . f
 F1 . f = cod f by A5;
hence  F1 . f = F2 . f by A6; ::_thesis: verum
end;
hence  F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def27 defines dom GRCAT_1:def_27_:_
 for V being Group_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = dom V iff for f being Element of Morphs V holds b2 . f = dom f );

:: deftheorem Def28 defines cod GRCAT_1:def_28_:_
 for V being Group_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = cod V iff for f being Element of Morphs V holds b2 . f = cod f );

theorem Th31: :: GRCAT_1:31
for V being Group_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proof
let V be Group_DOMAIN; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) )
assume A1: S1[g,f] ; ::_thesis: ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
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  ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 ) by A1, A2, A3, A4; ::_thesis: verum
end;

theorem Th32: :: GRCAT_1:32
for V being Group_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proof
let V be Group_DOMAIN; ::_thesis: for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let g, f be Element of Morphs V; ::_thesis: ( dom g = cod f implies g * f in Morphs V )
assume  S1[g,f] ; ::_thesis: g * f in Morphs V
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  g * f in Morphs V by Def25; ::_thesis: verum
end;

definition
let V be Group_DOMAIN;
func comp V ->  PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def30: :: GRCAT_1:def 29
( ( 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
 ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
deffunc H1( Element of Morphs V, Element of Morphs V) ->  strict GroupMorphism = $1 * $2;
A1: for g, f being Element of Morphs V st S1[g,f] holds
H1(g,f) in Morphs V by Th32;
consider c being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) such that
A2: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff S1[g,f] ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = H1(g,f) ) ) from BINOP_1:sch_8(A1);
take  c ; ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) )
thus  ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c holds
c . (g,f) = g * f ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proof
set X = Morphs V;
defpred S1[ Element of Morphs V, Element of Morphs V] means  dom $1 = cod $2;
let c1, c2 be PartFunc of [:(Morphs V),(Morphs V):],(Morphs V); ::_thesis: ( ( for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ) implies c1 = c2 )
assume that
A3: for g, f being Element of Morphs V holds
( [g,f] in dom c1 iff S1[g,f] ) and
A4: for g, f being Element of Morphs V st [g,f] in dom c1 holds
c1 . (g,f) = g * f and
A5: for g, f being Element of Morphs V holds
( [g,f] in dom c2 iff S1[g,f] ) and
A6: for g, f being Element of Morphs V st [g,f] in dom c2 holds
c2 . (g,f) = g * f ; ::_thesis: c1 = c2
set V9 = dom c1;
A7: dom c1 c= [:(Morphs V),(Morphs V):] by RELAT_1:def_18;
now__::_thesis:_for_x_being_set_st_x_in_dom_c1_holds_
x_in_dom_c2
let x be set ; ::_thesis: ( x in dom c1 implies x in dom c2 )
assume A8: x in dom c1 ; ::_thesis: x in dom c2
then consider g, f being Element of Morphs V such that
A9: x = [g,f] by A7, SUBSET_1:43;
 S1[g,f] by A3, A8, A9;
hence  x in dom c2 by A5, A9; ::_thesis: verum
end;
then A10: dom c1 c= dom c2 by TARSKI:def_3;
A11: for x, y being set st [x,y] in dom c1 holds
c1 . (x,y) = c2 . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom c1 implies c1 . (x,y) = c2 . (x,y) )
assume A12: [x,y] in dom c1 ; ::_thesis: c1 . (x,y) = c2 . (x,y)
then reconsider x = x, y = y as Element of Morphs V by A7, ZFMISC_1:87;
 c1 . (x,y) = x * y by A4, A12;
hence  c1 . (x,y) = c2 . (x,y) by A6, A10, A12; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_dom_c2_holds_
x_in_dom_c1
let x be set ; ::_thesis: ( x in dom c2 implies x in dom c1 )
assume A13: x in dom c2 ; ::_thesis: x in dom c1
 dom c2 c= [:(Morphs V),(Morphs V):] by RELAT_1:def_18;
then consider g, f being Element of Morphs V such that
A14: x = [g,f] by A13, SUBSET_1:43;
 S1[g,f] by A5, A13, A14;
hence  x in dom c1 by A3, A14; ::_thesis: verum
end;
then  dom c2 c= dom c1 by TARSKI:def_3;
then  dom c1 = dom c2 by A10, XBOOLE_0:def_10;
hence  c1 = c2 by A11, BINOP_1:20; ::_thesis: verum
end;
end;

:: deftheorem Def30 defines comp GRCAT_1:def_29_:_
 for V being Group_DOMAIN
for b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b2 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) ) );

definition
let UN be Universe;
func GroupCat UN ->  non empty non void strict CatStr  equals :: GRCAT_1:def 30
 CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);
coherence
 CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #) is non empty non void strict CatStr ;
end;

:: deftheorem  defines GroupCat GRCAT_1:def_30_:_
 for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict ;
coherence
 ( GroupCat UN is strict & not GroupCat UN is void & not GroupCat UN is empty ) ;
end;

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

theorem Th34: :: GRCAT_1:34
for UN being Universe
for f being Morphism of (GroupCat UN)
for f9 being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for 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
let UN be Universe; ::_thesis: for f being Morphism of (GroupCat UN)
for f9 being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for 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) )
set C = GroupCat UN;
set V = GroupObjects UN;
set X = Morphs (GroupObjects UN);
let f be Morphism of (GroupCat UN); ::_thesis: for f9 being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for 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) )
let f9 be Element of Morphs (GroupObjects UN); ::_thesis: for b being Object of (GroupCat UN)
for 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) )
let b be Object of (GroupCat UN); ::_thesis: for 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) )
let b9 be Element of GroupObjects UN; ::_thesis: ( 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) )
consider x being set  such that
 x in UN and
A1: GO x,b by Def24;
 ex G, H being strict Element of GroupObjects UN st f is strict Morphism of G,H by Def25;
hence  f is strict Element of Morphs (GroupObjects UN) ; ::_thesis: ( f9 is Morphism of (GroupCat UN) & b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) )
thus  f9 is Morphism of (GroupCat UN) ; ::_thesis: ( b is strict Element of GroupObjects UN & b9 is Object of (GroupCat UN) )
 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 GroupObjects UN ; ::_thesis: b9 is Object of (GroupCat UN)
thus  b9 is Object of (GroupCat UN) ; ::_thesis: verum
end;

theorem :: GRCAT_1:35
canceled;

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

Lm1:  for UN being Universe
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
let UN be Universe; ::_thesis: for f, g being Morphism of (GroupCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
set X = Morphs (GroupObjects UN);
let f, g be Morphism of (GroupCat UN); ::_thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (GroupObjects UN) by Th34;
reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th34;
A2: dom g9 = cod f9 by A1, Th36;
then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th32;
A3: gf = g (*) f by A1, Th36;
 ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th20;
hence  ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th36; ::_thesis: verum
end;

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict Category-like reflexive ;
coherence
 ( GroupCat UN is reflexive & GroupCat UN is Category-like )
proof
set C = GroupCat UN;
thus  GroupCat UN is reflexive ::_thesis: GroupCat UN is Category-like
proof
let a be Element of (GroupCat UN); :: according to CAT_1:def_9 ::_thesis: not Hom (a,a) = {}
reconsider G = a as Element of GroupObjects UN ;
consider x being set  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 = G as strict Element of GroupObjects UN by W3;
reconsider ii = ID G as Morphism of (GroupCat UN) ;
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) <> {} ; ::_thesis: verum
end;
let f, g be Morphism of (GroupCat UN); :: according to CAT_1:def_6 ::_thesis: ( ( not [g,f] in proj1 the Comp of (GroupCat UN) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of (GroupCat UN) ) )
reconsider ff = f, gg = g as Element of Morphs (GroupObjects UN) ;
thus  ( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f ) by Th36; ::_thesis: verum
end;
end;

Lm3:  for UN being Universe
for a being Element of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
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 UN be Universe; ::_thesis: for a being Element of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
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 ) )
let a be Element of (GroupCat UN); ::_thesis: for aa being Element of GroupObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
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 ) )
let aa be Element of GroupObjects UN; ::_thesis: ( a = aa implies for i being Morphism of a,a st i = ID aa holds
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 ) ) )
assume  a = aa ; ::_thesis: for i being Morphism of a,a st i = ID aa holds
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 ) )
let i be Morphism of a,a; ::_thesis: ( i = ID aa implies 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 ) ) )
assume Z2: i = ID aa ; ::_thesis: 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 ) )
let b be Element of (GroupCat UN); ::_thesis: ( ( 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 ) )
thus  ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) ::_thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
proof
assume Z3: Hom (a,b) <> {} ; ::_thesis: for g being Morphism of a,b holds g (*) i = g
let g be Morphism of a,b; ::_thesis: g (*) i = g
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 = f as Function of aa,H1 ;
G1: GroupMorphismStr(# the Source of gg, the Target of gg, the Fun 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 ;
::_thesis: verum
end;
thus  ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ::_thesis: verum
proof
assume Z3: Hom (b,a) <> {} ; ::_thesis: for f being Morphism of b,a holds i (*) f = f
let g be Morphism of b,a; ::_thesis: i (*) g = g
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 = f as Function of G1,aa ;
G1: GroupMorphismStr(# the Source of gg, the Target of gg, the Fun 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 ;
::_thesis: verum
end;
end;

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict transitive associative with_identities ;
coherence
 ( GroupCat UN is transitive & GroupCat UN is associative & GroupCat UN is with_identities )
proof
set C = GroupCat UN;
set X = Morphs (GroupObjects UN);
thus  GroupCat UN is transitive ::_thesis: ( GroupCat UN is associative & GroupCat UN is with_identities )
proof
let f, g be Morphism of (GroupCat UN); :: according to CAT_1:def_7 ::_thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
assume A1: dom g = cod f ; ::_thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
reconsider g9 = g as strict Element of Morphs (GroupObjects UN) by Th34;
reconsider f9 = f as strict Element of Morphs (GroupObjects UN) by Th34;
A2: dom g9 = cod f9 by A1, Th36;
then reconsider gf = g9 * f9 as Element of Morphs (GroupObjects UN) by Th32;
A3: gf = g (*) f by A1, Th36;
 ( dom (g9 * f9) = dom f9 & cod (g9 * f9) = cod g9 ) by A2, Th20;
hence  ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by A3, Th36; ::_thesis: verum
end;
thus  GroupCat UN is associative ::_thesis: GroupCat UN is with_identities
proof
let f, g, h be Morphism of (GroupCat UN); :: according to CAT_1:def_8 ::_thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
assume A1: ( dom h = cod g & dom g = cod f ) ; ::_thesis: h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 = f, g9 = g, h9 = h as strict Element of Morphs (GroupObjects UN) 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 Morphs (GroupObjects UN) 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  h (*) (g (*) f) = (h (*) g) (*) f ; ::_thesis: verum
end;
thus  GroupCat UN is with_identities ::_thesis: verum
proof
let a be Element of (GroupCat UN); :: according to CAT_1:def_10 ::_thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )
reconsider aa = a as Element of GroupObjects UN ;
reconsider ii = ID aa as Morphism of (GroupCat UN) ;
reconsider ia = ii as GroupMorphismStr ;
A: dom ii = dom ia by Def27
.= a ;
cod ii = cod ia by Def28
.= a ;
then reconsider ii = ii as Morphism of a,a by A, CAT_1:4;
take  ii ; ::_thesis: for b1 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )
thus  for b1 being Element of the carrier of (GroupCat UN) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) ) by Lm3; ::_thesis: verum
end;
end;
end;

definition
let UN be Universe;
func AbGroupObjects UN ->  Subset of the carrier of (GroupCat UN) equals :: GRCAT_1:def 31
 {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  ;
coherence
  {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  is Subset of the carrier of (GroupCat UN)
proof
set D2 = the carrier of (GroupCat UN);
now__::_thesis:_for_x_being_set_st_x_in__{__G_where_G_is_Element_of_the_carrier_of_(GroupCat_UN)_:_ex_H_being_AbGroup_st_G_=_H__}__holds_
x_in_the_carrier_of_(GroupCat_UN)
let x be set ; ::_thesis: ( x in  {  G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H  }  implies x in the carrier of (GroupCat UN) )
assume  x in  {  G where G is Element of the carrier of (GroupCat UN) : ex H being AbGroup st G = H  }  ; ::_thesis: x in the carrier of (GroupCat UN)
then  ex G being Element of the carrier of (GroupCat UN) st
( x = G & ex H being AbGroup st G = H ) ;
hence  x in the carrier of (GroupCat UN) ; ::_thesis: verum
end;
hence   {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  is Subset of the carrier of (GroupCat UN) by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines AbGroupObjects GRCAT_1:def_31_:_
 for UN being Universe holds AbGroupObjects UN =  {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  ;

theorem Th37: :: GRCAT_1:37
for UN being Universe holds Trivial-addLoopStr in AbGroupObjects UN
proof
let UN be Universe; ::_thesis: Trivial-addLoopStr in AbGroupObjects UN
 Trivial-addLoopStr in the carrier of (GroupCat UN) by Th29;
hence  Trivial-addLoopStr in AbGroupObjects UN ; ::_thesis: verum
end;

registration
let UN be Universe;
cluster AbGroupObjects UN ->  non empty ;
coherence
 not AbGroupObjects UN is empty by Th37;
end;

definition
let UN be Universe;
func AbGroupCat UN ->  Subcategory of GroupCat UN equals :: GRCAT_1:def 32
 cat (AbGroupObjects UN);
coherence
 cat (AbGroupObjects UN) is Subcategory of GroupCat UN ;
end;

:: deftheorem  defines AbGroupCat GRCAT_1:def_32_:_
 for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN);

registration
let UN be Universe;
cluster AbGroupCat UN ->  strict ;
coherence
 AbGroupCat UN is strict ;
end;

theorem :: GRCAT_1:38
for UN being Universe holds the carrier of (AbGroupCat UN) = AbGroupObjects UN ;

definition
let UN be Universe;
func MidOpGroupObjects UN ->  Subset of the carrier of (AbGroupCat UN) equals :: GRCAT_1:def 33
 {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  ;
coherence
  {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  is Subset of the carrier of (AbGroupCat UN)
proof
set D2 = the carrier of (AbGroupCat UN);
now__::_thesis:_for_x_being_set_st_x_in__{__G_where_G_is_Element_of_the_carrier_of_(AbGroupCat_UN)_:_ex_H_being_midpoint_operator_AbGroup_st_G_=_H__}__holds_
x_in_the_carrier_of_(AbGroupCat_UN)
let x be set ; ::_thesis: ( x in  {  G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  implies x in the carrier of (AbGroupCat UN) )
assume  x in  {  G where G is Element of the carrier of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  ; ::_thesis: x in the carrier of (AbGroupCat UN)
then  ex G being Element of the carrier of (AbGroupCat UN) st
( x = G & ex H being midpoint_operator AbGroup st G = H ) ;
hence  x in the carrier of (AbGroupCat UN) ; ::_thesis: verum
end;
hence   {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  is Subset of the carrier of (AbGroupCat UN) by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines MidOpGroupObjects GRCAT_1:def_33_:_
 for UN being Universe holds MidOpGroupObjects UN =  {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  ;

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

definition
let UN be Universe;
func MidOpGroupCat UN ->  Subcategory of AbGroupCat UN equals :: GRCAT_1:def 34
 cat (MidOpGroupObjects UN);
coherence
 cat (MidOpGroupObjects UN) is Subcategory of AbGroupCat UN ;
end;

:: deftheorem  defines MidOpGroupCat GRCAT_1:def_34_:_
 for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN);

registration
let UN be Universe;
cluster MidOpGroupCat UN ->  strict ;
coherence
 MidOpGroupCat UN is strict ;
end;

theorem :: GRCAT_1:39
for UN being Universe holds the carrier of (MidOpGroupCat UN) = MidOpGroupObjects UN ;

theorem :: GRCAT_1:40
for UN being Universe holds Trivial-addLoopStr in MidOpGroupObjects UN
proof
let UN be Universe; ::_thesis: Trivial-addLoopStr in MidOpGroupObjects UN
 Trivial-addLoopStr in the carrier of (AbGroupCat UN) by Th37;
hence  Trivial-addLoopStr in MidOpGroupObjects UN ; ::_thesis: verum
end;

theorem :: GRCAT_1:41
for S, T being non empty 1-sorted
for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )
proof
let S, T be non empty 1-sorted ; ::_thesis: for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )
let f be Function of S,T; ::_thesis: ( f is one-to-one & f is onto implies ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) )
A1: [#] T = the carrier of T ;
assume A2: ( f is one-to-one & f is onto ) ; ::_thesis: ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is 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  ( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto ) by A2, A3, A1, FUNCT_2:def_3, TOPS_2:50, TOPS_2:52; ::_thesis: verum
end;

theorem :: GRCAT_1:42
for UN being Universe
for a being Object of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
proof
let UN be Universe; ::_thesis: for a being Object of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
let a be Object of (GroupCat UN); ::_thesis: for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
let aa be Element of GroupObjects UN; ::_thesis: ( a = aa implies id a = ID aa )
set C = GroupCat UN;
assume Z: a = aa ; ::_thesis: id a = ID aa
reconsider ii = ID aa as Morphism of (GroupCat UN) ;
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 = ii as Morphism of a,a by A, CAT_1:4;
 for b being Object of (GroupCat UN) 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; ::_thesis: verum
end;