deffunc H₁( object ) -> Element of bool [:(M . I),(M . I):] = id (M . I);
consider f being ManySortedSet of I such that
A1: for d being object st d in I holds
f . d = H₁(d) from PBOOLE:sch 4();
for i being set st i in I holds
f . i is Relation of (M . i),(M . i)

proof

let i be set ; :: thesis: ( i in I implies f . i is Relation of (M . i),(M . i) )
assume i in I ; :: thesis: f . i is Relation of (M . i),(M . i)
then f . i = id (M . i) by A1;
hence f . i is Relation of (M . i),(M . i) ; :: thesis: verum

end;

then reconsider f = f as ManySortedRelation of M by MSUALG_4:def 1;
take f ; :: thesis: f is MSEquivalence_Relation-like
for i being object
for R being Relation of (M . i) st i in I & f . 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 & f . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); :: thesis: ( i in I & f . i = R implies R is Equivalence_Relation of (M . i) )
assume that
A2: i in I and
A3: f . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
R = id (M . i) by A1, A2, A3;
hence R is Equivalence_Relation of (M . i) ; :: thesis: verum

end;

hence f is MSEquivalence_Relation-like by MSUALG_4:def 2; :: thesis: verum