let P, Q be Relation of (D * ); :: thesis: ( ( for x, y being FinSequence of D holds
( [x,y] in P iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) & ( for x, y being FinSequence of D holds
( [x,y] in Q iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) implies P = Q )
assume that
A4: for x, y being FinSequence of D holds
( [x,y] in P iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) and
A5: for x, y being FinSequence of D holds
( [x,y] in Q iff ( len x = len y & ( for n being Element of NAT st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ; :: thesis: P = Q
for a, b being set holds
( [a,b] in P iff [a,b] in Q )

proof

let a, b be set ; :: thesis: ( [a,b] in P iff [a,b] in Q )
thus ( [a,b] in P implies [a,b] in Q ) :: thesis: ( [a,b] in Q implies [a,b] in P )

proof

assume A6: [a,b] in P ; :: thesis: [a,b] in Q
then reconsider a1 = a, b1 = b as Element of D * by ZFMISC_1:106;
( len a1 = len b1 & ( for n being Element of NAT st n in dom a1 holds
[(a1 . n),(b1 . n)] in R ) ) by A4, A6;
hence [a,b] in Q by A5; :: thesis: verum

end;

assume A7: [a,b] in Q ; :: thesis: [a,b] in P
then reconsider a1 = a, b1 = b as Element of D * by ZFMISC_1:106;
( len a1 = len b1 & ( for n being Element of NAT st n in dom a1 holds
[(a1 . n),(b1 . n)] in R ) ) by A5, A7;
hence [a,b] in P by A4; :: thesis: verum

end;

hence P = Q by RELAT_1:def 2; :: thesis: verum