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)) and
A3: j in dom (SgmX (R,A)) and
A4: (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, A4, Def2; :: thesis: verum