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)

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

end;

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

let i be set ; :: thesis:
let R be Relation of (M . i); :: thesis:
assume that
A2: i in I and
A3: f . i = R ; :: thesis:
R = id (M . i) by A1, A2, A3;
hence R is Equivalence_Relation of (M . i) ; :: thesis:

end;