set C = GroupCat UN;
set X = Morphs (GroupObjects UN);
thus
GroupCat UN is transitive
( GroupCat UN is associative & GroupCat UN is with_identities )
thus
GroupCat UN is associative
GroupCat UN is with_identities proof
let f,
g,
h be
Morphism of
(GroupCat UN);
CAT_1:def 8 ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
assume A4:
(
dom h = cod g &
dom g = cod f )
;
h (*) (g (*) f) = (h (*) g) (*) f
reconsider f9 =
f,
g9 =
g,
h9 =
h as
strict Element of
Morphs (GroupObjects UN) by Th34;
A5:
(
h9 * g9 = h (*) g &
dom (h (*) g) = cod f )
by A4, Lm1, Th35;
A6:
(
dom h9 = cod g9 &
dom g9 = cod f9 )
by A4, Th35;
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 A4, Lm1, Th35;
then h (*) (g (*) f) =
h9 * gf
by Th35
.=
hg * f9
by A6, Th22
.=
(h (*) g) (*) f
by A5, Th35
;
hence
h (*) (g (*) f) = (h (*) g) (*) f
;
verum
end;
thus
GroupCat UN is with_identities
verumproof
let a be
Element of
(GroupCat UN);
CAT_1:def 10 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 ;
A7:
dom ii =
dom ia
by Def25
.=
a
;
cod ii =
cod ia
by Def26
.=
a
;
then reconsider ii =
ii as
Morphism of
a,
a by A7, CAT_1:4;
take
ii
;
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 Lm2;
verum
end;