let UN be Universe; 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]
; ( [[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; verum