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 )
proof
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 )
proof
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;
hence s = SgmX ( the InternalRel of A,B) by A1, PRE_POLY:9; :: thesis: verum
end;
A5: the InternalRel of A linearly_orders B by Th37, ORDERS_1:38;
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
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
proof
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;
hence s /. n < s /. m by A11, ORDERS_2:def 6; :: thesis: verum
end;
then s is ascending ;
hence s is B -asc_ordering by A7; :: thesis: verum