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 by PARTFUN1:def 4, RELAT_1:def 18;
M is non-empty ;
hence 0 .--> the carrier of A is V5() ManySortedSet of ; :: thesis: verum