let UN be Universe; :: thesis: for R being Ring
for x being Element of LModObjects UN,R holds x is strict LeftMod of R
let R be Ring; :: thesis: for x being Element of LModObjects UN,R holds x is strict LeftMod of R
let x be Element of LModObjects UN,R; :: thesis: x is strict LeftMod of R
set N = { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,1:],1 : verum } ;
consider u being set such that
A1: ( u in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs [:the carrier of R,1:],1 : verum } & GO u,x,R ) by Def6;
ex a1, a2 being set st
( u = [a1,a2] & ex G being strict LeftMod of R st
( x = G & a1 = addLoopStr(# the carrier of G,the addF of G,the U2 of G #) & a2 = the lmult of G ) ) by A1, Def5;
hence x is strict LeftMod of R ; :: thesis: verum