let UN be Universe; :: thesis: ex x being object st
( x in UN & GO x, Z_3 )
set G = Z_3 ;
reconsider x1 = the carrier of Z_3, x2 = the addF of Z_3, x3 = comp Z_3, x4 = 0. Z_3, x5 = the multF of Z_3, x6 = 1. Z_3 as Element of UN by MOD_2:29;
set x9 = [x1,x2,x3,x4];
set x = [[x1,x2,x3,x4],x5,x6];
take [[x1,x2,x3,x4],x5,x6] ; :: thesis: ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z_3 )
[x1,x2,x3,x4] is Element of UN by GRCAT_1:1;
hence ( [[x1,x2,x3,x4],x5,x6] in UN & GO [[x1,x2,x3,x4],x5,x6], Z_3 ) by GRCAT_1:1; :: thesis: verum