let UN be Universe; :: thesis: ex x being set st
( x in UN & GO x, Trivial-addLoopStr )
reconsider x2 = op2 as Element of UN by Th3;
reconsider x3 = comp Trivial-addLoopStr as Element of UN by Th3, Th6;
reconsider u = {} as Element of UN by CLASSES2:56;
set x1 = {u};
Extract {} = u ;
then reconsider x4 = Extract {} as Element of UN ;
reconsider x = [{u},x2,x3,x4] as set by TARSKI:1;
take x ; :: thesis: ( x in UN & GO x, Trivial-addLoopStr )
thus x in UN by Th1; :: thesis: GO x, Trivial-addLoopStr
take {u} ; :: according to GRCAT_1:def 23 :: thesis: ex x2, x3, x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take x2 ; :: thesis: ex x3, x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take x3 ; :: thesis: ex x4 being set st
( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
take x4 ; :: thesis: ( x = [{u},x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
thus x = [{u},x2,x3,x4] ; :: thesis: ex G being strict AddGroup st
( Trivial-addLoopStr = G & {u} = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G )
take Trivial-addLoopStr ; :: thesis: ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr )
thus ( Trivial-addLoopStr = Trivial-addLoopStr & {u} = the carrier of Trivial-addLoopStr & x2 = the addF of Trivial-addLoopStr & x3 = comp Trivial-addLoopStr & x4 = 0. Trivial-addLoopStr ) ; :: thesis: verum