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