set C = RingCat UN;
thus
RingCat UN is Category-like
by Th21; ( RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )
thus
RingCat UN is transitive
by Lm9; ( RingCat UN is associative & RingCat UN is reflexive )
thus
RingCat UN is associative
by Lm10; RingCat UN is reflexive
thus
RingCat UN is reflexive
verumproof
let a be
Element of
(RingCat UN);
CAT_1:def 9 not Hom (a,a) = {}
reconsider G =
a as
Element of
RingObjects UN ;
consider x being
set such that
x in UN
and A1:
GO x,
G
by Def16;
set ii =
ID G;
consider x1,
x2,
x3,
x4,
x5,
x6 being
set such that
x = [[x1,x2,x3,x4],x5,x6]
and A2:
ex
H being
strict Ring st
(
G = H &
x1 = the
carrier of
H &
x2 = the
addF of
H &
x3 = comp H &
x4 = 0. H &
x5 = the
multF of
H &
x6 = 1. H )
by A1;
reconsider G =
G as
strict Element of
RingObjects UN by A2;
reconsider ii =
ID G as
Morphism of
(RingCat UN) ;
reconsider ia =
ii as
RingMorphismStr ;
A3:
dom ii =
dom ia
by Def19
.=
a
;
cod ii =
cod ia
by Def20
.=
a
;
then
ii in Hom (
a,
a)
by A3;
hence
Hom (
a,
a)
<> {}
;
verum
end;