deffunc H_{1}( 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_{1}(d)
from PBOOLE:sch 4();

for i being set st i in I holds

f . i is Relation of (M . i),(M . i)

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)

consider f being ManySortedSet of I such that

A1: for d being object st d in I holds

f . d = H

for i being set st i in I holds

f . i is Relation of (M . i),(M . i)

proof

then reconsider f = f as ManySortedRelation of M by MSUALG_4:def 1;
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;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

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

hence
f is MSEquivalence_Relation-like
by MSUALG_4:def 2; :: thesis: verum
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

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;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