consider r being natural-valued finite-support ManySortedSet of X;
r = r ;
hence ex b₁ being ManySortedSet of X st
( b₁ is natural-valued & b₁ is finite-support ) ; :: thesis: verum