set C = LModCat (UN,R);
thus
LModCat (UN,R) is Category-like
by Th14; ( LModCat (UN,R) is transitive & LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
thus
LModCat (UN,R) is transitive
by Lm1; ( LModCat (UN,R) is associative & LModCat (UN,R) is reflexive )
thus
LModCat (UN,R) is associative
by Lm2; LModCat (UN,R) is reflexive
thus
LModCat (UN,R) is reflexive
verumproof
let a be
Element of
(LModCat (UN,R));
CAT_1:def 9 not Hom (a,a) = {}
reconsider G =
a as
Element of
LModObjects (
UN,
R) ;
consider x being
set such that
x in { [H,f] where H is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of H:], the carrier of H) : verum }
and A1:
GO x,
G,
R
by Def6;
set ii =
ID G;
consider x1,
x2 being
object such that
x = [x1,x2]
and A2:
ex
H being
strict LeftMod of
R st
(
G = H &
x1 = addLoopStr(# the
carrier of
H, the
addF of
H, the
ZeroF of
H #) &
x2 = the
lmult of
H )
by A1;
reconsider G =
G as
strict Element of
LModObjects (
UN,
R)
by A2;
reconsider ii =
ID G as
Morphism of
(LModCat (UN,R)) ;
reconsider ia =
ii as
LModMorphismStr over
R ;
A3:
dom ii =
dom ia
by Th13
.=
a
;
cod ii =
cod ia
by Th13
.=
a
;
then
ii in Hom (
a,
a)
by A3;
hence
Hom (
a,
a)
<> {}
;
verum
end;