let A be LinearOrder; :: thesis: for B being finite Subset of A

for s being FinSequence of A holds

( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

let B be finite Subset of A; :: thesis: for s being FinSequence of A holds

( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

let s be FinSequence of A; :: thesis: ( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

thus ( s is B -asc_ordering implies s = SgmX ( the InternalRel of A,B) ) :: thesis: ( s = SgmX ( the InternalRel of A,B) implies s is B -asc_ordering )

assume A6: s = SgmX ( the InternalRel of A,B) ; :: thesis: s is B -asc_ordering

then A7: rng s = B by A5, PRE_POLY:def 2;

A8: s is one-to-one by A5, A6, PRE_POLY:10;

for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. n < s /. m

hence s is B -asc_ordering by A7; :: thesis: verum

for s being FinSequence of A holds

( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

let B be finite Subset of A; :: thesis: for s being FinSequence of A holds

( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

let s be FinSequence of A; :: thesis: ( s is B -asc_ordering iff s = SgmX ( the InternalRel of A,B) )

thus ( s is B -asc_ordering implies s = SgmX ( the InternalRel of A,B) ) :: thesis: ( s = SgmX ( the InternalRel of A,B) implies s is B -asc_ordering )

proof

A5:
the InternalRel of A linearly_orders B
by Th37, ORDERS_1:38;
assume A1:
s is B -asc_ordering
; :: thesis: s = SgmX ( the InternalRel of A,B)

for n, m being Nat st n in dom s & m in dom s & n < m holds

( s /. n <> s /. m & [(s /. n),(s /. m)] in the InternalRel of A )

end;for n, m being Nat st n in dom s & m in dom s & n < m holds

( s /. n <> s /. m & [(s /. n),(s /. m)] in the InternalRel of A )

proof

hence
s = SgmX ( the InternalRel of A,B)
by A1, PRE_POLY:9; :: thesis: verum
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies ( s /. n <> s /. m & [(s /. n),(s /. m)] in the InternalRel of A ) )

assume A2: ( n in dom s & m in dom s & n < m ) ; :: thesis: ( s /. n <> s /. m & [(s /. n),(s /. m)] in the InternalRel of A )

then reconsider x = s . n, y = s . m as Element of A by PARTFUN1:4;

A3: ( x = s /. n & y = s /. m ) by A2, PARTFUN1:def 6;

A4: x < y by A1, A2, A3, Def19;

hence s /. n <> s /. m by A3; :: thesis: [(s /. n),(s /. m)] in the InternalRel of A

thus [(s /. n),(s /. m)] in the InternalRel of A by A3, A4, ORDERS_2:def 6, ORDERS_2:def 5; :: thesis: verum

end;assume A2: ( n in dom s & m in dom s & n < m ) ; :: thesis: ( s /. n <> s /. m & [(s /. n),(s /. m)] in the InternalRel of A )

then reconsider x = s . n, y = s . m as Element of A by PARTFUN1:4;

A3: ( x = s /. n & y = s /. m ) by A2, PARTFUN1:def 6;

A4: x < y by A1, A2, A3, Def19;

hence s /. n <> s /. m by A3; :: thesis: [(s /. n),(s /. m)] in the InternalRel of A

thus [(s /. n),(s /. m)] in the InternalRel of A by A3, A4, ORDERS_2:def 6, ORDERS_2:def 5; :: thesis: verum

assume A6: s = SgmX ( the InternalRel of A,B) ; :: thesis: s is B -asc_ordering

then A7: rng s = B by A5, PRE_POLY:def 2;

A8: s is one-to-one by A5, A6, PRE_POLY:10;

for n, m being Nat st n in dom s & m in dom s & n < m holds

s /. n < s /. m

proof

then
s is ascending
;
let n, m be Nat; :: thesis: ( n in dom s & m in dom s & n < m implies s /. n < s /. m )

assume that

A9: ( n in dom s & m in dom s ) and

A10: n < m ; :: thesis: s /. n < s /. m

[(s /. n),(s /. m)] in the InternalRel of A by A5, A6, A9, A10, PRE_POLY:def 2;

then A11: s /. n <= s /. m by ORDERS_2:def 5;

s /. n <> s /. m

end;assume that

A9: ( n in dom s & m in dom s ) and

A10: n < m ; :: thesis: s /. n < s /. m

[(s /. n),(s /. m)] in the InternalRel of A by A5, A6, A9, A10, PRE_POLY:def 2;

then A11: s /. n <= s /. m by ORDERS_2:def 5;

s /. n <> s /. m

proof

hence
s /. n < s /. m
by A11, ORDERS_2:def 6; :: thesis: verum
assume A12:
s /. n = s /. m
; :: thesis: contradiction

( s /. n = s . n & s /. m = s . m ) by A9, PARTFUN1:def 6;

then n = m by A8, A9, FUNCT_1:def 4, A12;

hence contradiction by A10; :: thesis: verum

end;( s /. n = s . n & s /. m = s . m ) by A9, PARTFUN1:def 6;

then n = m by A8, A9, FUNCT_1:def 4, A12;

hence contradiction by A10; :: thesis: verum

hence s is B -asc_ordering by A7; :: thesis: verum