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

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)

hence
EqCl EqR = EqR
by Def3; :: thesis: verumlet 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;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