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 ;
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 ; :: thesis: verum
end;
hence s = SgmX ( the InternalRel of A,B) by ; :: thesis: verum
end;
A5: the InternalRel of A linearly_orders B by ;
assume A6: s = SgmX ( the InternalRel of A,B) ; :: thesis: s is B -asc_ordering
then A7: rng s = B by ;
A8: s is one-to-one by ;
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 ;
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 ;
then n = m by ;
hence contradiction by A10; :: thesis: verum
end;
hence s /. n < s /. m by ; :: thesis: verum
end;
then s is ascending ;
hence s is B -asc_ordering by A7; :: thesis: verum