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, the carrier of G:], the carrier of G) : verum } ;
consider u being set such that
u in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } and
A1: GO u,x,R by Def6;
ex a1, a2 being object 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 ZeroF of G #) & a2 = the lmult of G ) ) by A1;
hence x is strict LeftMod of R ; :: thesis: verum