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

suppose n = 0 ; :: thesis: ex b₁ being a_partition of n st b₁ is one-to-one

then reconsider N = {} as a_partition of n by RVSUM_1:72, Def3;
N is one-to-one ;
hence ex b₁ being a_partition of n st b₁ is one-to-one ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: ex b₁ being a_partition of n st b₁ is one-to-one

then not 0 in rng <*n*> ;
then A8: <*n*> is non-zero by ORDINAL1:def 15;
Sum <*n*> = n by RVSUM_1:73;
then reconsider N = <*n*> as a_partition of n by A8, Def3;
N is one-to-one ;
hence ex b₁ being a_partition of n st b₁ is one-to-one ; :: thesis: verum

end;

end;