let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: 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 2;
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 21; :: thesis: verum