A1: ( the carrier of (MSSign A) = {0 } & the carrier' of (MSSign A) = dom (signature A) & the Arity of (MSSign A) = (*--> 0 ) * (signature A) & the ResultSort of (MSSign A) = (dom (signature A)) --> 0 ) by Def13;
set M = {0 } --> the carrier of A;
dom ({0 } --> the carrier of A) = the carrier of (MSSign A) by A1, FUNCOP_1:19;
then reconsider M = {0 } --> the carrier of A as ManySortedSet of the carrier of (MSSign A) by PBOOLE:def 3;
M is non-empty ;
hence 0 .--> the carrier of A is V5 ManySortedSet of the carrier of (MSSign A) ; :: thesis: verum