let UN be Universe; :: thesis: for R being Ring
for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R))
for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) holds
( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
let R be Ring; :: thesis: for f being Morphism of (LModCat (UN,R))
for f9 being Element of Morphs (LModObjects (UN,R))
for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) holds
( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
set C = LModCat (UN,R);
set V = LModObjects (UN,R);
set X = Morphs (LModObjects (UN,R));
let f be Morphism of (LModCat (UN,R)); :: thesis: for f9 being Element of Morphs (LModObjects (UN,R))
for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) holds
( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
let f9 be Element of Morphs (LModObjects (UN,R)); :: thesis: for b being Object of (LModCat (UN,R))
for b9 being Element of LModObjects (UN,R) holds
( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
let b be Object of (LModCat (UN,R)); :: thesis: for b9 being Element of LModObjects (UN,R) holds
( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
let b9 be Element of LModObjects (UN,R); :: thesis: ( f is strict Element of Morphs (LModObjects (UN,R)) & f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
consider x being set such that
x in { [G,ff] where G is Element of GroupObjects UN, ff is Element of Funcs ([: the carrier of R,1:],1) : verum } and
A1: GO x,b,R by Def6;
ex G, H being strict Element of LModObjects (UN,R) st f is strict Morphism of G,H by Def7;
hence f is strict Element of Morphs (LModObjects (UN,R)) ; :: thesis: ( f9 is Morphism of (LModCat (UN,R)) & b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
thus f9 is Morphism of (LModCat (UN,R)) ; :: thesis: ( b is strict Element of LModObjects (UN,R) & b9 is Object of (LModCat (UN,R)) )
ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of R st
( b = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) by A1, Def5;
hence b is strict Element of LModObjects (UN,R) ; :: thesis: b9 is Object of (LModCat (UN,R))
thus b9 is Object of (LModCat (UN,R)) ; :: thesis: verum