let A be antisymmetric RelStr ; :: thesis:
let B be Subset of A; :: thesis:
let s1, s2 be FinSequence of A; :: thesis:
assume that
A1: s1 is B -asc_ordering and
A2: s2 is B -asc_ordering ; :: thesis:
A3: ( s1 is ascending & s2 is ascending ) by A1, A2;
A4: ( rng s1 = B & rng s2 = B ) by A1, A2;
len s1 = len s2 by A1, A2, FINSEQ_1:48;
then dom s1 = Seg (len s2) by FINSEQ_1:def 3;
then A5: dom s1 = dom s2 by FINSEQ_1:def 3;
defpred S₁[ Nat] means ( $1 in dom s1 & $1 in dom s2 implies s1 /. $1 = s2 /. $1 );
A6: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis:
assume A7: for n being Nat st n < k holds
S₁[n] ; :: thesis:
assume A8: ( k in dom s1 & k in dom s2 ) ; :: thesis:
assume A9: s1 /. k <> s2 /. k ; :: thesis:
s2 . k in rng s1 by A4, A8, FUNCT_1:def 3;
then consider i being Nat such that
A10: ( i in dom s1 & s1 . i = s2 . k ) by FINSEQ_2:10;
s1 /. i = s2 . k by A10, PARTFUN1:def 6;
then A11: s1 /. i = s2 /. k by A8, PARTFUN1:def 6;
s1 . k in rng s2 by A4, A8, FUNCT_1:def 3;
then consider j being Nat such that
A12: ( j in dom s2 & s2 . j = s1 . k ) by FINSEQ_2:10;
s2 /. j = s1 . k by A12, PARTFUN1:def 6;
then A13: s2 /. j = s1 /. k by A8, PARTFUN1:def 6;
A14: k < i

assume k >= i ; :: thesis:

end;

end;

assume k >= j ; :: thesis:

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A6);
then A21: for k being Nat st k in dom s1 & k in dom s2 holds
s1 /. k = s2 /. k ;
for k being Nat st k in dom s1 holds
s1 . k = s2 . k

end;