set M = {0 } --> the carrier of A;
the carrier of (MSSign A) = {0 } by Def13;
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 V5() ManySortedSet of the carrier of (MSSign A) ; :: thesis: verum