set M = {0} --> the carrier of A;
the carrier of (MSSign A) = {0} by Def8;
then reconsider M = {0} --> the carrier of A as ManySortedSet of the carrier of (MSSign A) ;
M is non-empty ;
hence 0 .--> the carrier of A is non-empty ManySortedSet of the carrier of (MSSign A) ; :: thesis: verum