let MS be non void 1 -element segmental ManySortedSign ; for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
let A be non-empty MSAlgebra over MS; ( the carrier of MS = {0} implies MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) )
reconsider ff1 = (*--> 0) * (signature (1-Alg A)) as Function of (dom (signature (1-Alg A))),({0} *) by MSUALG_1:2;
A1:
MSSign (1-Alg A) = ManySortedSign(# {0},(dom (signature (1-Alg A))),ff1,((dom (signature (1-Alg A))) --> z) #)
by MSUALG_1:10;
dom the ResultSort of MS = the carrier' of MS
by FUNCT_2:def 1;
then A2:
rng the ResultSort of MS <> {}
by RELAT_1:42;
consider k being Nat such that
A3:
the carrier' of MS = Seg k
by MSUALG_1:def 7;
A4:
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #)
by MSUALG_1:def 14;
A5:
len (signature (1-Alg A)) = len the charact of (1-Alg A)
by UNIALG_1:def 4;
then A6: dom (signature (1-Alg A)) =
dom the charact of (1-Alg A)
by FINSEQ_3:29
.=
dom the Charact of A
by A4, MSUALG_1:def 13
.=
the carrier' of MS
by PARTFUN1:def 2
;
then A7:
the carrier' of MS = dom ff1
by FUNCT_2:def 1;
assume A8:
the carrier of MS = {0}
; MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
A9:
for x being object st x in the carrier' of MS holds
((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x
proof
let x be
object ;
( x in the carrier' of MS implies ((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x )
assume
x in the
carrier' of
MS
;
((*--> 0) * (signature (1-Alg A))) . x = the Arity of MS . x
then reconsider x =
x as
OperSymbol of
MS ;
x in Seg k
by A3;
then reconsider n =
x as
Nat ;
n in dom (signature (1-Alg A))
by A6;
then A10:
n in dom the
charact of
(1-Alg A)
by A5, FINSEQ_3:29;
reconsider h = the
charact of
(1-Alg A) . n as
PartFunc of
( the carrier of (1-Alg A) *), the
carrier of
(1-Alg A) ;
reconsider h =
h as non
empty homogeneous quasi_total PartFunc of
( the carrier of (1-Alg A) *), the
carrier of
(1-Alg A) by A10, MARGREL1:def 24;
set aa = the
Element of
dom h;
set ah =
arity h;
dom h c= the
carrier of
(1-Alg A) *
by RELAT_1:def 18;
then
the
Element of
dom h in the
carrier of
(1-Alg A) *
;
then reconsider bb = the
Element of
dom h as
FinSequence of the
carrier of
(1-Alg A) by FINSEQ_1:def 11;
A11:
bb in dom h
;
h =
the
Charact of
A . x
by A4, MSUALG_1:def 13
.=
Den (
x,
A)
by MSUALG_1:def 6
;
then
bb in Args (
x,
A)
by A11, FUNCT_2:def 1;
then
bb in (len (the_arity_of x)) -tuples_on (the_sort_of A)
by MSUALG_1:6;
then A12:
len (the_arity_of x) =
len bb
by CARD_1:def 7
.=
arity h
by MARGREL1:def 25
;
((*--> 0) * (signature (1-Alg A))) . x =
(*--> 0) . ((signature (1-Alg A)) . x)
by A6, FUNCT_1:13
.=
(*--> 0) . (arity h)
by A6, UNIALG_1:def 4
.=
(arity h) |-> 0
by FINSEQ_2:def 6
.=
the_arity_of x
by A8, A12, Th5
.=
the
Arity of
MS . x
by MSUALG_1:def 1
;
hence
((*--> 0) * (signature (1-Alg A))) . x = the
Arity of
MS . x
;
verum
end;
rng the ResultSort of MS c= {0}
by A8, RELAT_1:def 19;
then
( the carrier' of MS = dom the ResultSort of MS & rng the ResultSort of MS = {0} )
by A2, FUNCT_2:def 1, ZFMISC_1:33;
then
( the carrier' of MS = dom the Arity of MS & the ResultSort of (MSSign (1-Alg A)) = the ResultSort of MS )
by A1, A6, FUNCOP_1:9, FUNCT_2:def 1;
hence
MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #)
by A8, A1, A7, A9, FUNCT_1:2; verum