let UN be Universe; :: thesis: ex x being set st
( x in UN & GO x, Z3 )
set G = Z3 ;
reconsider x1 = the carrier of Z3 , x2 = the addF of Z3 , x3 = comp Z3 , x4 = 0. Z3 , x5 = the multF of Z3 , x6 = 1. Z3 as Element of UN by MOD_2:40;
set x' = [x1,x2,x3,x4];
set x = [[x1,x2,x3,x4],x5,x6];
A1: [x1,x2,x3,x4] is Element of UN by GRCAT_1:3;
A2: GO [[x1,x2,x3,x4],x5,x6], Z3

proof

take x1 ; :: according to RINGCAT1:def 16 :: thesis: ex x2, x3, x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
take x2 ; :: thesis: ex x3, x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
take x3 ; :: thesis: ex x4, x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
take x4 ; :: thesis: ex x5, x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
take x5 ; :: thesis: ex x6 being set st
( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
take x6 ; :: thesis: ( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) )
thus ( [[x1,x2,x3,x4],x5,x6] = [[x1,x2,x3,x4],x5,x6] & ex G being strict Ring st
( Z3 = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G & x5 = the multF of G & x6 = 1. G ) ) ; :: thesis: verum

end;

take [[x1,x2,x3,x4],x5,x6] ; :: thesis: ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z3 )
thus ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z3 ) by A1, A2, GRCAT_1:3; :: thesis: verum