:: deftheorem defines GO MODCAT_1:def 5 :
for x, y being object
for R being Ring holds
( GO x,y,R iff ex x1, x2 being object st
( x = [x1,x2] & ex G being strict LeftMod of R st
( y = G & x1 = addLoopStr(# the carrier of G, the addF of G, the ZeroF of G #) & x2 = the lmult of G ) ) );