defpred S1[ object , object ] means GO $1,$2,R;
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 } ;
A1:
for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2
by Th4;
consider Y being set such that
A2:
for y being object holds
( y in Y iff ex x being object 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 } & S1[x,y] ) )
from TARSKI:sch 1(A1);
take
Y
; for y being object holds
( y in Y 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 ) )
let y be object ; ( y in Y 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 ) )
thus
( y in Y implies 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 ) )
( 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 y in Y )proof
assume
y in Y
;
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 )
then
ex
x being
object 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 } &
S1[
x,
y] )
by A2;
hence
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 )
;
verum
end;
thus
( 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 y in Y )
by A2; verum