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);
MSUALG_2:def 3 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)
and A4:
the
charact of
A . i = OO
by FINSEQ_2:11;
A5:
len (signature A) = len the
charact of
A
by UNIALG_1:def 11;
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
;
MSUALG_2:def 2 ( 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 11
.=
{}
by Th1
;
hence
the
Arity of
(MSSign A) . i = {}
by A1, FUNCT_1:23;
the ResultSort of (MSSign A) . i = s
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;
verum
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 )
; verum