let R be Ring; for UN being Universe ex x being object st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )
let UN be Universe; ex x being object st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )
set T = TrivialLMod R;
reconsider x1 = addLoopStr(# the carrier of (TrivialLMod R), the addF of (TrivialLMod R), the ZeroF of (TrivialLMod R) #) as Element of GroupObjects UN by GRCAT_1:29;
reconsider f1 = the lmult of (TrivialLMod R) as Function of [: the carrier of R,{{}}:],{{}} ;
reconsider x2 = f1 as Element of Funcs ([: the carrier of R,{{}}:],{{}}) by FUNCT_2:8;
take x = [x1,x2]; ( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum } & GO x, TrivialLMod R,R )
thus
x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R,{{}}:],{{}}) : verum }
; GO x, TrivialLMod R,R
thus
GO x, TrivialLMod R,R
; verum