let mu be natural-valued FinSequence; :: thesis: ( ( for j being Nat holds mu . (2 * j) = 0 ) implies ex h being odd-valued FinSequence st
( h is non-decreasing & ( for j being Nat holds card (Coim (h,j)) = mu . j ) ) )
assume A1: for j being Nat holds mu . (2 * j) = 0 ; :: thesis: ex h being odd-valued FinSequence st
( h is non-decreasing & ( for j being Nat holds card (Coim (h,j)) = mu . j ) )
set S = Seg (len mu);
A2: rng mu c= NAT by VALUED_0:def 6;
A3: dom mu = Seg (len mu) by FINSEQ_1:def 3;
then mu is Function of (Seg (len mu)),NAT by A2, FUNCT_2:2;
then consider h being FinSequence of Seg (len mu) such that
A4: for d being Element of Seg (len mu) holds card (Coim (h,d)) = mu . d by Th7;
A5: rng h c= Seg (len mu) by FINSEQ_1:def 4;
A6: rng h c= OddNAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in OddNAT )
assume A7: y in rng h ; :: thesis: y in OddNAT
then A8: card (Coim (h,y)) = mu . y by A4, A5;
Coim (h,y) = h " {y} by RELAT_1:def 17;
then A9: Coim (h,y) <> {} by A7, FUNCT_1:72;
consider x being object such that
A10: ( x in dom h & h . x = y ) by A7, FUNCT_1:def 3;
reconsider y = y as Nat by A10;
y is odd

proof

assume y is even ; :: thesis: contradiction
then ex j being Nat st y = 2 * j by ABIAN:def 2;
hence contradiction by A1, A9, A8; :: thesis: verum

end;

hence y in OddNAT by Th2; :: thesis: verum

end;

then reconsider h = h as odd-valued FinSequence by Def1;
rng h c= REAL ;
then reconsider h = h as FinSequence of REAL by FINSEQ_1:def 4;
set s = sort_a h;
rng h = rng (sort_a h) by RFINSEQ2:def 6, CLASSES1:75;
then reconsider s = sort_a h as odd-valued FinSequence by A6, Def1;
take s ; :: thesis: ( s is non-decreasing & ( for j being Nat holds card (Coim (s,j)) = mu . j ) )
thus s is non-decreasing ; :: thesis: for j being Nat holds card (Coim (s,j)) = mu . j
let i be Nat; :: thesis: card (Coim (s,i)) = mu . i

per cases ( i in Seg (len mu) or not i in Seg (len mu) ) ;

suppose i in Seg (len mu) ; :: thesis: card (Coim (s,i)) = mu . i

then mu . i = card (Coim (h,i)) by A4;
hence card (Coim (s,i)) = mu . i by RFINSEQ2:def 6, CLASSES1:def 10; :: thesis: verum

end;

suppose A11: not i in Seg (len mu) ; :: thesis: card (Coim (s,i)) = mu . i

then A12: ( mu . i = 0 & not i in rng h ) by A5, A3, FUNCT_1:def 2;
h " {i} = {} by A11, A5, FUNCT_1:72;
then Coim (h,i) = {} by RELAT_1:def 17;
then card (Coim (h,i)) = 0 ;
hence card (Coim (s,i)) = mu . i by CLASSES1:def 10, RFINSEQ2:def 6, A12; :: thesis: verum

end;

end;