let f be SetPrimes -defined natural-valued finite-support Function; :: thesis: ( f is increasing implies for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
sort_a F is one-to-one )
assume A1: f is increasing ; :: thesis: for F being real-valued FinSequence st F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) holds
sort_a F is one-to-one
set b = (EmptyBag SetPrimes) +* f;
set C = canFS (support ((EmptyBag SetPrimes) +* f));
let F be real-valued FinSequence; :: thesis: ( F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) implies sort_a F is one-to-one )
assume A2: F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) ; :: thesis: sort_a F is one-to-one
set S = sort_a F;
A3: F, sort_a F are_fiberwise_equipotent by RFINSEQ2:def 6;
A4: rng (canFS (support ((EmptyBag SetPrimes) +* f))) = support ((EmptyBag SetPrimes) +* f) by FUNCT_2:def 3;
A5: support ((EmptyBag SetPrimes) +* f) = support f by Th12;
A6: support f c= dom f by PRE_POLY:37;
let e1, e2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not e1 in proj1 (sort_a F) or not e2 in proj1 (sort_a F) or not (sort_a F) . e1 = (sort_a F) . e2 or e1 = e2 )
assume that
A7: ( e1 in dom (sort_a F) & e2 in dom (sort_a F) ) and
A8: (sort_a F) . e1 = (sort_a F) . e2 and
A9: e1 <> e2 ; :: thesis: contradiction
consider z1, z2 being set such that
A10: ( z1 in dom F & z2 in dom F ) and
A11: z1 <> z2 and
A12: ( F . z1 = (sort_a F) . e1 & F . z2 = (sort_a F) . e2 ) by A3, A7, A9, CONVEX2:13;
A13: ( z1 in dom (canFS (support ((EmptyBag SetPrimes) +* f))) & z2 in dom (canFS (support ((EmptyBag SetPrimes) +* f))) ) by A2, A10, Th13;
then A14: (canFS (support ((EmptyBag SetPrimes) +* f))) . z1 <> (canFS (support ((EmptyBag SetPrimes) +* f))) . z2 by A11, FUNCT_1:def 4;
A15: ( (canFS (support ((EmptyBag SetPrimes) +* f))) . z1 in rng (canFS (support ((EmptyBag SetPrimes) +* f))) & (canFS (support ((EmptyBag SetPrimes) +* f))) . z2 in rng (canFS (support ((EmptyBag SetPrimes) +* f))) ) by A13, FUNCT_1:def 3;
then ( ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z1) = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z1) & ((EmptyBag SetPrimes) +* f) . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z2) = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z2) ) by A4, A5, A6, FUNCT_4:13;
then ( F . z1 = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z1) & F . z2 = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z2) ) by A2, A10, FUNCT_1:12;
hence contradiction by A1, A4, A5, A6, A8, A12, A14, A15, FUNCT_1:def 4; :: thesis: verum