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 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 Nat st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ) implies P = Q )
assume that
A3: for x, y being FinSequence of D holds
( [x,y] in P iff ( len x = len y & ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R ) ) ) and
A4: for x, y being FinSequence of D holds
( [x,y] in Q iff ( len x = len y & ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in R ) ) ) ; :: thesis: P = Q
for a, b being object holds
( [a,b] in P iff [a,b] in Q )

proof

let a, b be object ; :: 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 A5: [a,b] in P ; :: thesis: [a,b] in Q
then reconsider a1 = a, b1 = b as Element of D * by ZFMISC_1:87;
( len a1 = len b1 & ( for n being Nat st n in dom a1 holds
[(a1 . n),(b1 . n)] in R ) ) by A3, A5;
hence [a,b] in Q by A4; :: thesis: verum

end;

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

end;

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