reconsider ff1 = (*--> 0 ) * (signature A) as Function of (dom (signature A)),({0 } * ) by MSUALG_1:7;
A1: MSSign A = ManySortedSign(# {0 },(dom (signature A)),ff1,((dom (signature A)) --> z) #) by MSUALG_1:16;
MSSign A is all-with_const_op

proof

let s be SortSymbol of (MSSign A); :: according to MSUALG_2:def 3 :: thesis: s is with_const_op
consider OO being operation of A such that
A2: arity OO = 0 by UNIALG_2:def 12;
Seg (len the charact of A) = dom the charact of A by FINSEQ_1:def 3;
then consider i being Nat such that
A3: ( i in Seg (len the charact of A) & the charact of A . i = OO ) by FINSEQ_2:11;
A4: len (signature A) = len the charact of A by UNIALG_1:def 11;
then A5: i in dom (signature A) by A3, FINSEQ_1:def 3;
reconsider i = i as OperSymbol of (MSSign A) by A1, A3, A4, FINSEQ_1:def 3;
take i ; :: according to MSUALG_2:def 2 :: thesis: ( the Arity of (MSSign A) . i = {} & the ResultSort of (MSSign A) . i = s )
thus the Arity of (MSSign A) . i = {} :: thesis: the ResultSort of (MSSign A) . i = s

proof

(*--> 0 ) . ((signature A) . i) = (*--> 0 ) . 0 by A2, A3, A5, UNIALG_1:def 11
.= {} by Th1 ;
hence the Arity of (MSSign A) . i = {} by A1, FUNCT_1:23; :: thesis: verum

end;

thus the ResultSort of (MSSign A) . i = s :: thesis: verum

proof

the ResultSort of (MSSign A) . i = 0 by A1, TARSKI:def 1;
hence the ResultSort of (MSSign A) . i = s by A1, TARSKI:def 1; :: thesis: verum

end;

end;

hence ( not MSSign A is void & MSSign A is strict & MSSign A is segmental & MSSign A is trivial & MSSign A is all-with_const_op ) ; :: thesis: verum