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
the Sorts of A = the Sorts of (MSAlg (1-Alg A))
let A be non-empty MSAlgebra over 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 :: thesis: for i being object st i in the carrier of MS holds
the Sorts of A . i = ({0} --> (the_sort_of A)) . i
let i be object ; :: 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:139;
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:7;
hence the Sorts of A . i = ({0} --> (the_sort_of A)) . i by A4, MSUALG_1:def 12; :: thesis: verum
end;
1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #) by MSUALG_1:def 14;
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 9, MSUALG_1:def 11;
{0} --> (the_sort_of A) is ManySortedSet of the carrier of MS by A1;
hence the Sorts of A = the Sorts of (MSAlg (1-Alg A)) by A5, A2, PBOOLE:3; :: thesis: verum