let s be SortSymbol of (MSSign A); :: according to MSUALG_2:def 2 :: thesis: s is with_const_op
consider OO being operation of A such that
A2: arity OO = 0 by UNIALG_2:def 11;
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) and
A4: the charact of A . i = OO by FINSEQ_2:10;
A5: len (signature A) = len the charact of A by UNIALG_1:def 4;
then A6: i in dom (signature A) by A3, FINSEQ_1:def 3;
reconsider i = i as OperSymbol of (MSSign A) by A1, A3, A5, FINSEQ_1:def 3;
take i ; :: according to MSUALG_2:def 1 :: thesis: ( the Arity of (MSSign A) . i = {} & the ResultSort of (MSSign A) . i = s )
(*--> 0) . ((signature A) . i) = (*--> 0) . 0 by A2, A4, A6, UNIALG_1:def 4
.= {} by Th1 ;
hence the Arity of (MSSign A) . i = {} by A1, FUNCT_1:13; :: thesis: the ResultSort of (MSSign A) . i = s
thus the ResultSort of (MSSign A) . i = s by A1, TARSKI:def 1; :: thesis: verum