let UN be Universe; :: thesis: for R being Ring holds TrivialLMod R in LModObjects (UN,R)
let R be Ring; :: thesis: TrivialLMod R in LModObjects (UN,R)
set G0 = Trivial-addLoopStr ;
set f0 = pr2 ( the carrier of R,{0});
reconsider G0 = Trivial-addLoopStr as Element of GroupObjects UN by GRCAT_1:29;
reconsider f0 = pr2 ( the carrier of R,{0}) as Element of Funcs ([: the carrier of R, the carrier of G0:], the carrier of G0) by FUNCT_2:8;
set x = [G0,f0];
A1: [G0,f0] 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 [G0,f0], TrivialLMod R,R ;
hence TrivialLMod R in LModObjects (UN,R) by A1, Def6; :: thesis: verum