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