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 Z2:
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 Z3:
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 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
;
verum
end;
thus
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
verumproof
assume Z3:
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 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
;
verum
end;