let MS be non empty trivial non void segmental ManySortedSign ; for A being non-empty MSAlgebra of 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 of 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:7;
A1:
MSSign (1-Alg A) = ManySortedSign(# {0 },(dom (signature (1-Alg A))),ff1,((dom (signature (1-Alg A))) --> z) #)
by MSUALG_1:16;
dom the ResultSort of MS = the carrier' of MS
by FUNCT_2:def 1;
then A2:
rng the ResultSort of MS <> {}
by RELAT_1:65;
consider k being Nat such that
A3:
the carrier' of MS = Seg k
by MSUALG_1:def 12;
A4:
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #)
by MSUALG_1:def 19;
A5:
len (signature (1-Alg A)) = len the charact of (1-Alg A)
by UNIALG_1:def 11;
then A6: dom (signature (1-Alg A)) =
dom the charact of (1-Alg A)
by FINSEQ_3:31
.=
dom the Charact of A
by A4, MSUALG_1:def 18
.=
the carrier' of MS
by PARTFUN1:def 4
;
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 set st x in the carrier' of MS holds
((*--> 0 ) * (signature (1-Alg A))) . x = the Arity of MS . x
proof
let x be
set ;
( 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:31;
then reconsider h = the
charact of
(1-Alg A) . n as
PartFunc of
(the carrier of (1-Alg A) * ),the
carrier of
(1-Alg A) by UNIALG_1:5;
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 25;
consider aa being
Element of
dom h;
set ah =
arity h;
dom h c= the
carrier of
(1-Alg A) *
by RELAT_1:def 18;
then
aa in the
carrier of
(1-Alg A) *
by TARSKI:def 3;
then reconsider bb =
aa 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 18
.=
Den x,
A
by MSUALG_1:def 11
;
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:11;
then A12:
len (the_arity_of x) =
len bb
by FINSEQ_1:def 18
.=
arity h
by MARGREL1:def 26
;
((*--> 0 ) * (signature (1-Alg A))) . x =
(*--> 0 ) . ((signature (1-Alg A)) . x)
by A6, FUNCT_1:23
.=
(*--> 0 ) . (arity h)
by A6, UNIALG_1:def 11
.=
(arity h) |-> 0
by PBOOLE:def 20
.=
the_arity_of x
by A8, A12, Th5
.=
the
Arity of
MS . x
by MSUALG_1:def 6
;
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:39;
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:15, 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, A6, A7, A9, FUNCT_1:9; verum