let A be LinearOrder; 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; 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; ( 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) )
( s = SgmX ( the InternalRel of A,B) implies s is B -asc_ordering )proof
assume A1:
s is
B -asc_ordering
;
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;
( 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 )
;
( 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;
[(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;
verum
end;
hence
s = SgmX ( the
InternalRel of
A,
B)
by A1, PRE_POLY:9;
verum
end;
A5:
the InternalRel of A linearly_orders B
by Th37, ORDERS_1:38;
assume A6:
s = SgmX ( the InternalRel of A,B)
; 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
then
s is ascending
;
hence
s is B -asc_ordering
by A7; verum