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 ;
then dom s1 = Seg (len s2) by FINSEQ_1:def 3;
then A5: dom s1 = dom s2 by FINSEQ_1:def 3;
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )

assume A7: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[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 ;
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 ;
then A11: s1 /. i = s2 /. k by ;
s1 . k in rng s2 by ;
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 ;
then A13: s2 /. j = s1 /. k by ;
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;
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;
end;
end;
s1 /. k < s1 /. i by A8, A10, A14, A3;
then A20: s1 /. k <= s2 /. k by ;
s2 /. k < s2 /. j by A8, A12, A17, A3;
then s2 /. k <= s1 /. k by ;
then s1 /. k = s2 /. k by ;
hence contradiction by A9; :: thesis: verum
end;
for k being Nat holds S1[k] from 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 ;
then s1 . k = s2 /. k by ;
hence s1 . k = s2 . k by ; :: thesis: verum
end;
then for k being object st k in dom s1 holds
s1 . k = s2 . k ;
hence s1 = s2 by ; :: thesis: verum