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

proof

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

end;

then reconsider f = f as ManySortedRelation of I by MSUALG_4:def 1;
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,M by MSUALG_4:def 2;
reconsider f = f as ManySortedRelation of M ;
take f ; :: thesis: f is MSEquivalence_Relation-like
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)

proof

let i be set ; :: 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
A3: i in I and
A4: f . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
R = id (M . i) by A1, A3, A4;
hence R is Equivalence_Relation of (M . i) ; :: thesis: verum

end;

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