let UN be Universe; 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
; ( x in UN & GO x, Trivial-addLoopStr )
thus
x in UN
by Th1; GO x, Trivial-addLoopStr
take
{u}
; GRCAT_1:def 23 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
; 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
; 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
; ( 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]
; 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
; ( 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 )
; verum