let U be Universe; :: thesis: for x being Element of U ex y being Element of U st GO y, Trivial-addLoopStr x
let x be Element of U; :: thesis: ex y being Element of U st GO y, Trivial-addLoopStr x
set Tx = Trivial-addLoopStr x;
reconsider x1 = {x} as Element of U ;
reconsider x2 = op2 x as Element of U by Th78;
reconsider x3 = comp (Trivial-addLoopStr x) as Element of U by Th79;
reconsider x4 = op0 x as Element of U ;
reconsider y = [x1,x2,x3,x4] as Element of U ;

now :: thesis: ex y being Element of U st
( y = [x1,x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )

take y = y; :: thesis: ( y = [x1,x2,x3,x4] & ex G being strict AddGroup st
( Trivial-addLoopStr x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) )
thus y = [x1,x2,x3,x4] ; :: thesis: ex G being strict AddGroup st
( Trivial-addLoopStr x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G )
x4 = 0. (Trivial-addLoopStr x) by TARSKI:def 1;
hence ex G being strict AddGroup st
( Trivial-addLoopStr x = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) ; :: thesis: verum

end;

hence ex y being Element of U st GO y, Trivial-addLoopStr x by GRCAT_1:def 23; :: thesis: verum