deffunc H₁( Element of I) -> Equivalence_Relation of = 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

proof

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

end;

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

proof

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

end;

then reconsider EqR = EqR as Equivalence_Relation of M by MSUALG_4:def 3;
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