let UN be Universe; for a being Element of (RingCat UN)
for aa being Element of RingObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
for b being Element of (RingCat 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 (RingCat UN); for aa being Element of RingObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
for b being Element of (RingCat 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 RingObjects UN; ( a = aa implies for i being Morphism of a,a st i = ID aa holds
for b being Element of (RingCat 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 (RingCat 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 (RingCat 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 (RingCat 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 (RingCat 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 (RingObjects UN) ;
consider G1,
H1 being
Element of
RingObjects UN such that W0:
G1 <= H1
and W1:
gg is
Morphism of
G1,
H1
by Def17;
consider f being
Function of
G1,
H1 such that W2:
gg = RingMorphismStr(#
G1,
H1,
f #)
by W0, W1, Lm8;
E:
Hom (
a,
a)
<> {}
by CAT_1:def 9;
CC1:
dom g =
a
by Z3, CAT_1:5
.=
cod i
by E, CAT_1:5
;
then C1:
dom gg = cod ii
by Th24;
then reconsider f =
f as
Function of
aa,
H1 by W2, Z2;
A:
[gg,ii] in dom (comp (RingObjects UN))
by Th24, CC1;
hence g (*) i =
(comp (RingObjects UN)) . (
g,
i)
by CAT_1:def 1
.=
gg * ii
by A, Def22
.=
RingMorphismStr(#
aa,
H1,
(f * (id aa)) #)
by Z2, Def9, W2, C1
.=
g
by Z2, W2, C1, FUNCT_2:17
;
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 (RingObjects UN) ;
consider G1,
H1 being
Element of
RingObjects UN such that W0:
G1 <= H1
and W1:
gg is
Morphism of
G1,
H1
by Def17;
consider f being
Function of
G1,
H1 such that W2:
gg = RingMorphismStr(#
G1,
H1,
f #)
by W0, W1, Lm8;
E:
Hom (
a,
a)
<> {}
by CAT_1:def 9;
CC1:
cod g =
a
by Z3, CAT_1:5
.=
dom i
by E, CAT_1:5
;
then C1:
cod gg = dom ii
by Th24;
reconsider f =
f as
Function of
G1,
aa by W2, Z2, C1;
A:
[ii,gg] in dom (comp (RingObjects UN))
by CC1, Th24;
hence i (*) g =
(comp (RingObjects UN)) . (
i,
g)
by CAT_1:def 1
.=
ii * gg
by A, Def22
.=
RingMorphismStr(#
G1,
aa,
((id aa) * f) #)
by Z2, Def9, W2, C1
.=
g
by Z2, C1, W2, FUNCT_2:17
;
verum
end;