per cases ( n <> 0 or n = 0 ) ;

suppose n <> 0 ; :: thesis: ex b₁ being non-zero natural-valued non-decreasing FinSequence st Sum b₁ = 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 b₁ being non-zero natural-valued non-decreasing FinSequence st Sum b₁ = n by A1; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ex b₁ being non-zero natural-valued non-decreasing FinSequence st Sum b₁ = n

hence ex b₁ being non-zero natural-valued non-decreasing FinSequence st Sum b₁ = n by RVSUM_1:72; :: thesis: verum

end;

end;