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