per cases ( n = 0 or n is odd or ( n is even & n <> 0 ) ) ;
suppose n = 0 ; :: thesis: ex b1 being a_partition of n st b1 is odd-valued
then reconsider N = {} as a_partition of n by RVSUM_1:72, Def3;
N is odd-valued ;
hence ex b1 being a_partition of n st b1 is odd-valued ; :: thesis: verum
end;
suppose A1: n is odd ; :: thesis: ex b1 being a_partition of n st b1 is odd-valued
Sum <*n*> = n by RVSUM_1:73;
then <*n*> is a_partition of n by Def3, A1;
hence ex b1 being a_partition of n st b1 is odd-valued by A1; :: thesis: verum
end;
suppose A2: ( n is even & n <> 0 ) ; :: thesis: ex b1 being a_partition of n st b1 is odd-valued
then consider i being Nat such that
A3: n = 2 * i by ABIAN:def 2;
i <> 0 by A2, A3;
then reconsider i1 = i - 1 as Nat ;
A4: ((i1 * 2) + 1) + 1 = n by A3;
A5: 1 = 1 + (2 * 0) ;
reconsider N1 = <*1*>, N2 = <*((i1 * 2) + 1)*> as natural-valued non-decreasing FinSequence ;
len N1 = 1 by FINSEQ_1:39;
then ( N1 . (len N1) = 1 & N2 . 1 = (i1 * 2) + 1 ) by FINSEQ_1:40;
then A6: N1 ^ N2 is non-decreasing by NAT_1:11, Th1;
rng <*1,((i1 * 2) + 1)*> = {1,((i1 * 2) + 1)} by FINSEQ_2:127;
then A7: <*1,((i1 * 2) + 1)*> is non-zero ;
N1 ^ N2 = <*1,((i1 * 2) + 1)*> ;
then Sum (N1 ^ N2) = n by RVSUM_1:77, A4;
then reconsider N = N1 ^ N2 as a_partition of n by A7, A6, Def3;
N is odd-valued by A5;
hence ex b1 being a_partition of n st b1 is odd-valued ; :: thesis: verum
end;
end;