take N = NAT * ; :: thesis: for b₁ being a_partition of n holds b₁ in N
let p be a_partition of n; :: thesis: p in N
rng p c= NAT by VALUED_0:def 6;
then p is FinSequence of NAT by FINSEQ_1:def 4;
hence p in N by FINSEQ_1:def 11; :: thesis: verum