let UN be Universe; for R being Ring
for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
let R be Ring; for x being Element of LModObjects (UN,R) holds x is strict LeftMod of R
let x be Element of LModObjects (UN,R); 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
; verum