let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
let M be ManySortedSet of I; :: thesis: for EqR being Equivalence_Relation of M holds EqCl EqR = EqR
let EqR be Equivalence_Relation of M; :: thesis: EqCl EqR = EqR

now :: thesis: for i being Element of I holds EqR . i = EqCl (EqR . i)

let i be Element of I; :: thesis: EqR . i = EqCl (EqR . i)
reconsider ER = EqR . i as Equivalence_Relation of (M . i) by MSUALG_4:def 2;
thus EqR . i = EqCl ER by Th2
.= EqCl (EqR . i) ; :: thesis: verum

end;

hence EqCl EqR = EqR by Def3; :: thesis: verum