per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: ex b1 being a_partition of n st b1 is one-to-one
then reconsider N = {} as a_partition of n by RVSUM_1:72, Def3;
N is one-to-one ;
hence ex b1 being a_partition of n st b1 is one-to-one ; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: ex b1 being a_partition of n st b1 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 b1 being a_partition of n st b1 is one-to-one ; :: thesis: verum
end;
end;