let X be set ; :: thesis: for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, j being Element of NAT st i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j holds
i = j
let A be finite Subset of X; :: thesis: for R being Order of X st R linearly_orders A holds
for i, j being Element of NAT st i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j holds
i = j
let R be Order of X; :: thesis: ( R linearly_orders A implies for i, j being Element of NAT st i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j holds
i = j )
assume A1: R linearly_orders A ; :: thesis: for i, j being Element of NAT st i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j holds
i = j
let i, j be Element of NAT ; :: thesis: ( i in dom (SgmX R,A) & j in dom (SgmX R,A) & (SgmX R,A) /. i = (SgmX R,A) /. j implies i = j )
assume that
A2: ( i in dom (SgmX R,A) & j in dom (SgmX R,A) ) and
A3: (SgmX R,A) /. i = (SgmX R,A) /. j ; :: thesis: i = j
assume i <> j ; :: thesis: contradiction
then ( i < j or j < i ) by XXREAL_0:1;
hence contradiction by A1, A2, A3, TRIANG_1:def 2; :: thesis: verum