let MS be non empty trivial non void segmental ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of MS st the carrier of MS = {0 } holds
the Sorts of A = the Sorts of (MSAlg (1-Alg A))
let A be non-empty MSAlgebra of MS; :: thesis: ( the carrier of MS = {0 } implies the Sorts of A = the Sorts of (MSAlg (1-Alg A)) )
assume A1: the carrier of MS = {0 } ; :: thesis: the Sorts of A = the Sorts of (MSAlg (1-Alg A))

A2: now

let i be set ; :: thesis: ( i in the carrier of MS implies the Sorts of A . i = ({0 } --> (the_sort_of A)) . i )
assume A3: i in the carrier of MS ; :: thesis: the Sorts of A . i = ({0 } --> (the_sort_of A)) . i
A4: ex c being Component of the Sorts of A st the Sorts of A . i = c

proof

reconsider c = the Sorts of A . i as Component of the Sorts of A by A3, PBOOLE:151;
take c ; :: thesis: the Sorts of A . i = c
thus the Sorts of A . i = c ; :: thesis: verum

end;

({0 } --> (the_sort_of A)) . i = the_sort_of A by A1, A3, FUNCOP_1:13;
hence the Sorts of A . i = ({0 } --> (the_sort_of A)) . i by A4, MSUALG_1:def 17; :: thesis: verum

end;

1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def 19;
then A5: ( MSAlg (1-Alg A) = MSAlgebra(# (MSSorts (1-Alg A)),(MSCharact (1-Alg A)) #) & MSSorts (1-Alg A) = 0 .--> (the_sort_of A) ) by MSUALG_1:def 14, MSUALG_1:def 16;
dom ({0 } --> (the_sort_of A)) = {0 } by FUNCOP_1:19;
then {0 } --> (the_sort_of A) is ManySortedSet of the carrier of MS by A1, PARTFUN1:def 4;
hence the Sorts of A = the Sorts of (MSAlg (1-Alg A)) by A5, A2, PBOOLE:3; :: thesis: verum