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