set N = { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } ;
let Y1, Y2 be set ; ( ( for y being object holds
( y in Y1 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) ) ) & ( for y being object holds
( y in Y2 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) ) ) implies Y1 = Y2 )
assume that
A3:
for y being object holds
( y in Y1 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) )
and
A4:
for y being object holds
( y in Y2 iff ex x being set st
( x in { [G,f] where G is Element of GroupObjects UN, f is Element of Funcs ([: the carrier of R, the carrier of G:], the carrier of G) : verum } & GO x,y,R ) )
; Y1 = Y2
hence
Y1 = Y2
by TARSKI:2; verum