let X be set ; :: thesis: for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) is one-to-one
let A be finite Subset of X; :: thesis: for R being Order of X st R linearly_orders A holds
SgmX (R,A) is one-to-one
let R be Order of X; :: thesis: ( R linearly_orders A implies SgmX (R,A) is one-to-one )
set f = SgmX (R,A);
assume A1: R linearly_orders A ; :: thesis: SgmX (R,A) is one-to-one
then rng (SgmX (R,A)) = A by Def2;
then reconsider f = SgmX (R,A) as FinSequence of A by FINSEQ_1:def 4;
f is one-to-one
proof
let k, l be object ; :: according to FUNCT_1:def 4 :: thesis: ( not k in dom f or not l in dom f or not f . k = f . l or k = l )
assume that
A2: k in dom f and
A3: l in dom f and
A4: f . k = f . l ; :: thesis: k = l
reconsider k = k, l = l as Element of NAT by A2, A3;
reconsider fk = f . k as Element of A by A2, FINSEQ_2:11;
reconsider fl = f . l as Element of A by A3, FINSEQ_2:11;
A5: fl = f /. l by A3, PARTFUN1:def 6;
A6: fk = f /. k by A2, PARTFUN1:def 6;
now :: thesis: not k <> l
A7: f /. l = f . l by A3, PARTFUN1:def 6
.= (SgmX (R,A)) /. l by A3, PARTFUN1:def 6 ;
A8: f /. k = f . k by A2, PARTFUN1:def 6
.= (SgmX (R,A)) /. k by A2, PARTFUN1:def 6 ;
assume A9: k <> l ; :: thesis: contradiction
per cases ( k < l or l < k ) by A9, XXREAL_0:1;
suppose k < l ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2; :: thesis: verum
end;
suppose l < k ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A4, A6, A5, A8, A7, Def2; :: thesis: verum
end;
end;
end;
hence k = l ; :: thesis: verum
end;
hence SgmX (R,A) is one-to-one ; :: thesis: verum