let X be non empty set ; :: thesis: for A being non empty finite Subset of X
for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX (R,A)) /. (len (SgmX (R,A))) = x
let A be non empty finite Subset of X; :: thesis: for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX (R,A)) /. (len (SgmX (R,A))) = x
let R be Order of X; :: thesis: for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX (R,A)) /. (len (SgmX (R,A))) = x
let x be Element of X; :: thesis: ( x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) implies (SgmX (R,A)) /. (len (SgmX (R,A))) = x )
assume that
A1: x in A and
A2: R linearly_orders A and
A3: for y being Element of X st y in A holds
[y,x] in R and
A4: (SgmX (R,A)) /. (len (SgmX (R,A))) <> x ; :: thesis: contradiction
set L = len (SgmX (R,A));
A5: A = rng (SgmX (R,A)) by A2, Def2;
then consider i being Element of NAT such that
A6: i in dom (SgmX (R,A)) and
A7: (SgmX (R,A)) /. i = x by A1, PARTFUN2:2;
not SgmX (R,A) is empty by A2, Def2, RELAT_1:38;
then A8: len (SgmX (R,A)) in dom (SgmX (R,A)) by FINSEQ_5:6;
then A9: [((SgmX (R,A)) /. (len (SgmX (R,A)))),x] in R by A3, A5, PARTFUN2:2;
A10: field R = X by ORDERS_1:12;
i <= len (SgmX (R,A)) by A6, FINSEQ_3:25;
then i < len (SgmX (R,A)) by A4, A7, XXREAL_0:1;
then [x,((SgmX (R,A)) /. (len (SgmX (R,A))))] in R by A2, A6, A7, A8, Def2;
hence contradiction by A4, A9, A10, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum