let UN be Universe; :: thesis: for R being Ring
for f being Morphism of
for f' being Element of Morphs (LModObjects UN,R)
for b being Object of
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
let R be Ring; :: thesis: for f being Morphism of
for f' being Element of Morphs (LModObjects UN,R)
for b being Object of
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
set C = LModCat UN,R;
set V = LModObjects UN,R;
set X = Morphs (LModObjects UN,R);
let f be Morphism of ; :: thesis: for f' being Element of Morphs (LModObjects UN,R)
for b being Object of
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
let f' be Element of Morphs (LModObjects UN,R); :: thesis: for b being Object of
for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
let b be Object of ; :: thesis: for b' being Element of LModObjects UN,R holds
( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
let b' be Element of LModObjects UN,R; :: thesis: ( f is strict Element of Morphs (LModObjects UN,R) & f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
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: ( f' is Morphism of & b is strict Element of LModObjects UN,R & b' is Object of )
thus f' is Morphism of ; :: thesis: ( b is strict Element of LModObjects UN,R & b' is Object of )
ex x1, x2 being set st
( x = [x1,x2] & ex G being strict LeftMod of strict 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
thus b' is Object of ; :: thesis: verum