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 V5() ;
hence 0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A) ; :: thesis: verum