let R be Ring; :: thesis: 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; :: thesis: 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]; :: thesis: ( 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 } ; :: thesis: GO x, TrivialLMod R,R
thus GO x, TrivialLMod R,R ; :: thesis: verum