let R1, R2 be Relation of [: the carrier of TS,(E ^omega):]; :: thesis: ( ( 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 ) ; :: thesis: R1 = R2

now :: thesis: 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):]; :: thesis: ( [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; :: thesis: verum

end;

hence R1 = R2 by RELSET_1:def 2; :: thesis: verum