let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
let A be non-empty MSAlgebra over S; :: thesis: for C being MSCongruence of A st C = [| the Sorts of A, the Sorts of A|] holds
the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}
let C be MSCongruence of A; :: thesis: ( C = [| the Sorts of A, the Sorts of A|] implies the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} )
assume A1: C = [| the Sorts of A, the Sorts of A|] ; :: thesis: the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A}

now :: thesis: for i being object st i in the carrier of S holds
the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i

let i be object ; :: thesis: ( i in the carrier of S implies the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i )
assume i in the carrier of S ; :: thesis: the Sorts of (QuotMSAlg (A,C)) . i = { the Sorts of A} . i
then reconsider s = i as Element of S ;
A2: C . s = [:( the Sorts of A . s),( the Sorts of A . s):] by A1, PBOOLE:def 16
.= nabla ( the Sorts of A . s) by EQREL_1:def 1 ;
thus the Sorts of (QuotMSAlg (A,C)) . i = Class (C . s) by MSUALG_4:def 6
.= {( the Sorts of A . s)} by A2, Th4
.= { the Sorts of A} . i by PZFMISC1:def 1 ; :: thesis: verum

end;

hence the Sorts of (QuotMSAlg (A,C)) = { the Sorts of A} ; :: thesis: verum