:: deftheorem Def6 defines LModObjects MODCAT_1:def 6 :
for UN being Universe
for R being Ring
for b₃ being set holds
( b₃ = LModObjects (UN,R) iff for y being object holds
( y in b₃ iff ex x being set st
( x 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 } & GO x,y,R ) ) );