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 increasing )
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 increasing
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 increasing )
assume A2: F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) ; :: thesis: sort_a F is increasing
set S = sort_a F;
A3: F, sort_a F are_fiberwise_equipotent by RFINSEQ2:def 6;
A4: dom (((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f)))) = dom (canFS (support ((EmptyBag SetPrimes) +* f))) by Th13;
A5: rng (canFS (support ((EmptyBag SetPrimes) +* f))) = support ((EmptyBag SetPrimes) +* f) by FUNCT_2:def 3;
A6: support ((EmptyBag SetPrimes) +* f) = support f by Th12;
A7: support f c= dom f by PRE_POLY:37;
let e1, e2 be Nat; :: according to SEQM_3:def 1 :: thesis: ( not e1 in proj1 (sort_a F) or not e2 in proj1 (sort_a F) or e2 <= e1 or not (sort_a F) . e2 <= (sort_a F) . e1 )
assume that
A8: ( e1 in dom (sort_a F) & e2 in dom (sort_a F) ) and
A9: e1 < e2 ; :: thesis: not (sort_a F) . e2 <= (sort_a F) . e1
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, A8, A9, CONVEX2:13;
A13: (canFS (support ((EmptyBag SetPrimes) +* f))) . z1 <> (canFS (support ((EmptyBag SetPrimes) +* f))) . z2 by A2, A4, A10, A11, FUNCT_1:def 4;
A14: ( (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 A2, A4, A10, 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 A5, A6, A7, FUNCT_4:13;
then A15: ( F . z1 = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z1) & F . z2 = f . ((canFS (support ((EmptyBag SetPrimes) +* f))) . z2) ) by A2, A10, FUNCT_1:12;
(sort_a F) . e1 <= (sort_a F) . e2 by A8, A9, RFINSEQ2:17;
hence not (sort_a F) . e2 <= (sort_a F) . e1 by A1, A5, A6, A7, A12, A13, A14, A15, FUNCT_1:def 4, XXREAL_0:1; :: thesis: verum