let A be antisymmetric RelStr ; :: thesis: for B being Subset of A
for s1, s2 being FinSequence of A st s1 is B -asc_ordering & s2 is B -asc_ordering holds
s1 = s2
let B be Subset of A; :: thesis: for s1, s2 being FinSequence of A st s1 is B -asc_ordering & s2 is B -asc_ordering holds
s1 = s2
let s1, s2 be FinSequence of A; :: thesis: ( s1 is B -asc_ordering & s2 is B -asc_ordering implies s1 = s2 )
assume that
A1: s1 is B -asc_ordering and
A2: s2 is B -asc_ordering ; :: thesis: s1 = s2
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]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A7: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
assume A8: ( k in dom s1 & k in dom s2 ) ; :: thesis: s1 /. k = s2 /. k
assume A9: s1 /. k <> s2 /. k ; :: thesis: contradiction
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

proof

assume k >= i ; :: thesis: contradiction

per cases then ( i < k or i = k ) by XXREAL_0:1;

suppose A15: i < k ; :: thesis: contradiction

then A16: s1 /. i = s2 /. i by A7, A10, A5;
s2 /. i < s2 /. k by A15, A10, A3, A5, A8;
hence contradiction by A11, A16; :: thesis: verum

end;

suppose i = k ; :: thesis: contradiction

then s1 /. k = s2 . k by A10, PARTFUN1:def 6;
hence contradiction by A9, A8, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

A17: k < j

proof

assume k >= j ; :: thesis: contradiction

per cases then ( j < k or j = k ) by XXREAL_0:1;

suppose A18: j < k ; :: thesis: contradiction

then A19: s1 /. j = s2 /. j by A7, A12, A5;
s1 /. j < s1 /. k by A18, A12, A3, A5, A8;
hence contradiction by A13, A19; :: thesis: verum

end;

suppose j = k ; :: thesis: contradiction

then s1 /. k = s2 . k by A8, A12, PARTFUN1:def 6;
hence contradiction by A9, A8, PARTFUN1:def 6; :: thesis: verum

end;

end;

end;

s1 /. k < s1 /. i by A8, A10, A14, A3;
then A20: s1 /. k <= s2 /. k by A11, ORDERS_2:def 6;
s2 /. k < s2 /. j by A8, A12, A17, A3;
then s2 /. k <= s1 /. k by A13, ORDERS_2:def 6;
then s1 /. k = s2 /. k by A20, ORDERS_2:2;
hence contradiction by A9; :: thesis: verum

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

proof

let k be Nat; :: thesis: ( k in dom s1 implies s1 . k = s2 . k )
assume A22: k in dom s1 ; :: thesis: s1 . k = s2 . k
then s1 /. k = s2 /. k by A21, A5;
then s1 . k = s2 /. k by A22, PARTFUN1:def 6;
hence s1 . k = s2 . k by A22, A5, PARTFUN1:def 6; :: thesis: verum

end;

then for k being object st k in dom s1 holds
s1 . k = s2 . k ;
hence s1 = s2 by A5, FUNCT_1:2; :: thesis: verum