deffunc H₁( Element of I) -> Equivalence_Relation of (M . $1) = EqCl (R . $1);
consider EqR being ManySortedSet of I such that
A1: for i being Element of I holds EqR . i = H₁(i) from PBOOLE:sch 5();
for i being set st i in I holds
EqR . i is Relation of (M . i)

proof

let i be set ; :: thesis: ( i in I implies EqR . i is Relation of (M . i) )
assume i in I ; :: thesis: EqR . i is Relation of (M . i)
then reconsider i9 = i as Element of I ;
EqR . i = EqCl (R . i9) by A1;
hence EqR . i is Relation of (M . i) ; :: thesis: verum

end;

then reconsider EqR = EqR as ManySortedRelation of M by MSUALG_4:def 1;
for i being object
for R being Relation of (M . i) st i in I & EqR . i = R holds
R is Equivalence_Relation of (M . i)

proof

let i be object ; :: thesis: for R being Relation of (M . i) st i in I & EqR . i = R holds
R is Equivalence_Relation of (M . i)
let R1 be Relation of (M . i); :: thesis: ( i in I & EqR . i = R1 implies R1 is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: EqR . i = R1 ; :: thesis: R1 is Equivalence_Relation of (M . i)
reconsider i9 = i as Element of I by A2;
R1 = EqCl (R . i9) by A1, A3;
hence R1 is Equivalence_Relation of (M . i) ; :: thesis: verum

end;

then reconsider EqR = EqR as Equivalence_Relation of M by MSUALG_4:def 2;
take EqR ; :: thesis: for i being Element of I holds EqR . i = EqCl (R . i)
thus for i being Element of I holds EqR . i = EqCl (R . i) by A1; :: thesis: verum