let UN be 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 ) )
let a be 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 aa be Element of GroupObjects UN; ( 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
; 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; ( 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 A1:
i = ID aa
; for b being Element of (GroupCat UN) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
let b be Element of (GroupCat UN); ( ( 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 )
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )proof
assume A2:
Hom (
a,
b)
<> {}
;
for g being Morphism of a,b holds g (*) i = g
let g be
Morphism of
a,
b;
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 A3:
gg is
strict Morphism of
G1,
H1
by Def23;
consider f being
Function of
G1,
H1 such that A4:
gg = GroupMorphismStr(#
G1,
H1,
f #)
by A3, Th13;
A5:
ii = GroupMorphismStr(#
aa,
aa,
(id aa) #)
by A1;
A6:
cod ii = aa
by A1;
A7:
dom gg = G1
by A4;
A8:
Hom (
a,
a)
<> {}
;
dom g =
a
by A2, CAT_1:5
.=
cod i
by A8, CAT_1:5
;
then A9:
dom gg = cod ii
by Th35;
then
aa = dom gg
by A6;
then A10:
aa = G1
by A7;
then reconsider f =
f as
Function of
aa,
H1 ;
A11:
GroupMorphismStr(# the
Source of
gg, the
Target of
gg, the
Fun of
gg #)
= GroupMorphismStr(#
aa,
H1,
f #)
by A4, A10;
A12:
[gg,ii] in dom (comp (GroupObjects UN))
by Def27, A9;
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 A12, Def27
.=
GroupMorphismStr(#
aa,
H1,
(f * (id aa)) #)
by A5, Def14, A11, A9
.=
GroupMorphismStr(#
aa,
H1,
f #)
by FUNCT_2:17
.=
g
by A10, A4
;
verum
end;
thus
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
verumproof
assume A13:
Hom (
b,
a)
<> {}
;
for f being Morphism of b,a holds i (*) f = f
let g be
Morphism of
b,
a;
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 A14:
gg is
strict Morphism of
G1,
H1
by Def23;
consider f being
Function of
G1,
H1 such that A15:
gg = GroupMorphismStr(#
G1,
H1,
f #)
by A14, Th13;
A16:
ii = GroupMorphismStr(#
aa,
aa,
(id aa) #)
by A1;
A17:
dom ii = aa
by A1;
A18:
cod gg = H1
by A15;
A19:
Hom (
a,
a)
<> {}
;
cod g =
a
by A13, CAT_1:5
.=
dom i
by A19, CAT_1:5
;
then A20:
cod gg = dom ii
by Th35;
then
aa = cod gg
by A17;
then A21:
aa = H1
by A18;
then reconsider f =
f as
Function of
G1,
aa ;
A22:
GroupMorphismStr(# the
Source of
gg, the
Target of
gg, the
Fun of
gg #)
= GroupMorphismStr(#
G1,
aa,
f #)
by A15, A21;
A23:
[ii,gg] in dom (comp (GroupObjects UN))
by Def27, A20;
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 A23, Def27
.=
GroupMorphismStr(#
G1,
aa,
((id aa) * f) #)
by A16, Def14, A22, A20
.=
GroupMorphismStr(#
G1,
aa,
f #)
by FUNCT_2:17
.=
g
by A21, A15
;
verum
end;