let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
let A be non-empty MSAlgebra over S; :: thesis: for C being MSCongruence of A holds C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
let C be MSCongruence of A; :: thesis: C is ManySortedSubset of [| the Sorts of A, the Sorts of A|]
set SF = the Sorts of A;
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in the carrier of S or C . i c= [| the Sorts of A, the Sorts of A|] . i )
assume A1: i in the carrier of S ; :: thesis: C . i c= [| the Sorts of A, the Sorts of A|] . i
C . i is Relation of ( the Sorts of A . i),( the Sorts of A . i) by A1, MSUALG_4:def 1;
then C . i c= [:( the Sorts of A . i),( the Sorts of A . i):] ;
hence C . i c= [| the Sorts of A, the Sorts of A|] . i by A1, PBOOLE:def 16; :: thesis: verum