per cases ( n <> 0 or n = 0 ) ;
suppose n <> 0 ; :: thesis: ex b1 being non-zero natural-valued non-decreasing FinSequence st Sum b1 = n
then not 0 in rng <*n*> ;
then A1: <*n*> is non-zero by ORDINAL1:def 15;
Sum <*n*> = n by RVSUM_1:73;
hence ex b1 being non-zero natural-valued non-decreasing FinSequence st Sum b1 = n by A1; :: thesis: verum
end;
suppose n = 0 ; :: thesis: ex b1 being non-zero natural-valued non-decreasing FinSequence st Sum b1 = n
hence ex b1 being non-zero natural-valued non-decreasing FinSequence st Sum b1 = n by RVSUM_1:72; :: thesis: verum
end;
end;