let R1, R2 be Relation of [: the carrier of TS,(E ^omega):]; ( ( for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ) implies R1 = R2 )
assume that
A12:
for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS )
and
A13:
for x1, x2, y1, y2 being object holds
( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS )
; R1 = R2
now for s, t being Element of [: the carrier of TS,(E ^omega):] holds
( [s,t] in R1 iff [s,t] in R2 )let s,
t be
Element of
[: the carrier of TS,(E ^omega):];
( [s,t] in R1 iff [s,t] in R2 )consider x,
u being
object such that A14:
x in the
carrier of
TS
and A15:
u in E ^omega
and A16:
s = [x,u]
by ZFMISC_1:def 2;
reconsider u =
u as
Element of
E ^omega by A15;
reconsider x =
x as
Element of
TS by A14;
consider y,
v being
object such that A17:
y in the
carrier of
TS
and A18:
v in E ^omega
and A19:
t = [y,v]
by ZFMISC_1:def 2;
reconsider v =
v as
Element of
E ^omega by A18;
reconsider y =
y as
Element of
TS by A17;
(
[s,t] in R1 iff
x,
u ==>. y,
v,
TS )
by A12, A16, A19;
hence
(
[s,t] in R1 iff
[s,t] in R2 )
by A13, A16, A19;
verum end;
hence
R1 = R2
by RELSET_1:def 2; verum