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_{1}[ 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_{1}[n] ) holds

S_{1}[k]
_{1}[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

s1 . k = s2 . k ;

hence s1 = s2 by A5, FUNCT_1:2; :: thesis: verum

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

A6: for k being Nat st ( for n being Nat st n < k holds

S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A7: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[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

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;S

assume A7: for n being Nat st n < k holds

S

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

A17:
k < j
assume
k >= i
; :: thesis: contradiction

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

end;

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;s2 /. i < s2 /. k by A15, A10, A3, A5, A8;

hence contradiction by A11, A16; :: thesis: verum

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;hence contradiction by A9, A8, PARTFUN1:def 6; :: thesis: verum

proof

s1 /. k < s1 /. i
by A8, A10, A14, A3;
assume
k >= j
; :: thesis: contradiction

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

end;

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;s1 /. j < s1 /. k by A18, A12, A3, A5, A8;

hence contradiction by A13, A19; :: thesis: verum

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;hence contradiction by A9, A8, PARTFUN1:def 6; :: thesis: verum

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

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

then
for k being object st k in dom s1 holds
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;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

s1 . k = s2 . k ;

hence s1 = s2 by A5, FUNCT_1:2; :: thesis: verum