let UN be Universe; :: thesis: for R being Ring
for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R)
for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
let R be Ring; :: thesis: for f being Morphism of (LModCat UN,R)
for f' being Element of Morphs (LModObjects UN,R)
for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' 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 f' being Element of Morphs (LModObjects UN,R)
for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
let f' be Element of Morphs (LModObjects UN,R); :: thesis: for b being Object of (LModCat UN,R)
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
let b be Object of (LModCat UN,R); :: thesis: for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
let b' be Element of LModObjects UN,R; :: thesis: ( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
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: ( f' is Morphism of (LModCat UN,R) & b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
thus f' is Morphism of (LModCat UN,R) ; :: thesis: ( b is strict Element of LModObjects UN,R & b' is Object of (LModCat UN,R) )
consider x being set such that
A1: ( x in { [G,ff] where G is Element of GroupObjects UN, ff is Element of Funcs [:the carrier of R,1:],1 : verum } & GO x,b,R ) by Def6;
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 U2 of G #) & x2 = the lmult of G ) ) by A1, Def5;
hence b is strict Element of LModObjects UN,R ; :: thesis: b' is Object of (LModCat UN,R)
thus b' is Object of (LModCat UN,R) ; :: thesis: verum