let MS be non void 1 -element segmental ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over MS st the carrier of MS = {0} holds
MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
let A be non-empty MSAlgebra over MS; :: thesis: ( the carrier of MS = {0} implies MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) )
reconsider c = the_sort_of (MSAlg (1-Alg A)) as Component of the Sorts of (MSAlg (1-Alg A)) by MSUALG_1:def 12;
assume the carrier of MS = {0} ; :: thesis: MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #)
then MSSign (1-Alg A) = ManySortedSign(# the carrier of MS, the carrier' of MS, the Arity of MS, the ResultSort of MS #) by Th23;
then reconsider M1A = MSAlg (1-Alg A) as strict MSAlgebra over MS ;
reconsider M1A = M1A as strict non-empty MSAlgebra over MS by MSUALG_1:def 3;
A1: 1-Alg M1A = UAStr(# (the_sort_of M1A),(the_charact_of M1A) #) by MSUALG_1:def 14;
reconsider c = c as Component of the Sorts of M1A ;
A2: 1-Alg (MSAlg (1-Alg A)) = UAStr(# (the_sort_of (MSAlg (1-Alg A))),(the_charact_of (MSAlg (1-Alg A))) #) by MSUALG_1:def 14;
then A3: the charact of (1-Alg A) = the_charact_of (MSAlg (1-Alg A)) by MSUALG_1:9
.= the Charact of M1A by MSUALG_1:def 13
.= the charact of (1-Alg M1A) by A1, MSUALG_1:def 13 ;
c = the_sort_of M1A by MSUALG_1:def 12;
then the carrier of (1-Alg A) = the carrier of (1-Alg M1A) by A2, A1, MSUALG_1:9;
hence MSAlg (1-Alg A) = MSAlgebra(# the Sorts of A, the Charact of A #) by A3, Th24; :: thesis: verum