let R be Ring; :: thesis: for UN being Universe 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,1:],1 : verum } & GO x, TrivialLMod R,R )
let UN be Universe; :: thesis: 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,1:],1 : verum } & GO x, TrivialLMod R,R )
set T = TrivialLMod R;
A1: TrivialLMod R = VectSpStr(# 1,op2 ,op0 ,(pr2 the carrier of R,1) #) by MOD_2:def 2;
then 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:42;
reconsider f1 = the lmult of (TrivialLMod R) as Function of [:the carrier of R,1:],1 by A1;
reconsider x2 = f1 as Element of Funcs [:the carrier of R,1:],1 by FUNCT_2:11;
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,1:],1 : 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,1:],1 : verum } ; :: thesis: GO x, TrivialLMod R,R
thus GO x, TrivialLMod R,R by Def5; :: thesis: verum