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 A1:
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 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 (RingObjects UN) ;
consider G1,
H1 being
Element of
RingObjects UN such that A3:
G1 <= H1
and A4:
gg is
Morphism of
G1,
H1
by Def17;
consider f being
Function of
G1,
H1 such that A5:
gg = RingMorphismStr(#
G1,
H1,
f #)
by A3, A4, Lm8;
A6:
Hom (
a,
a)
<> {}
by CAT_1:def 9;
A7:
dom g =
a
by A2, CAT_1:5
.=
cod i
by A6, CAT_1:5
;
then A8:
dom gg = cod ii
by Th23;
then reconsider f =
f as
Function of
aa,
H1 by A5, A1;
A9:
[gg,ii] in dom (comp (RingObjects UN))
by Th23, A7;
hence g (*) i =
(comp (RingObjects UN)) . (
g,
i)
by CAT_1:def 1
.=
gg * ii
by A9, Def21
.=
RingMorphismStr(#
aa,
H1,
(f * (id aa)) #)
by A1, Def9, A5, A8
.=
g
by A1, A5, A8, FUNCT_2:17
;
verum
end;
thus
( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f )
verumproof
assume A10:
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 A11:
G1 <= H1
and A12:
gg is
Morphism of
G1,
H1
by Def17;
consider f being
Function of
G1,
H1 such that A13:
gg = RingMorphismStr(#
G1,
H1,
f #)
by A11, A12, Lm8;
A14:
Hom (
a,
a)
<> {}
by CAT_1:def 9;
A15:
cod g =
a
by A10, CAT_1:5
.=
dom i
by A14, CAT_1:5
;
then A16:
cod gg = dom ii
by Th23;
reconsider f =
f as
Function of
G1,
aa by A13, A1, A16;
A17:
[ii,gg] in dom (comp (RingObjects UN))
by A15, Th23;
hence i (*) g =
(comp (RingObjects UN)) . (
i,
g)
by CAT_1:def 1
.=
ii * gg
by A17, Def21
.=
RingMorphismStr(#
G1,
aa,
((id aa) * f) #)
by A1, Def9, A13, A16
.=
g
by A1, A16, A13, FUNCT_2:17
;
verum
end;