deffunc H_{1}( Element of I) -> Equivalence_Relation of (M . $1) = EqCl (R . $1);

consider EqR being ManySortedSet of I such that

A1: for i being Element of I holds EqR . i = H_{1}(i)
from PBOOLE:sch 5();

for i being set st i in I holds

EqR . i is Relation of (M . i)

for i being set

for R being Relation of (M . i) st i in I & EqR . i = R holds

R is Equivalence_Relation of (M . i)

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

consider EqR being ManySortedSet of I such that

A1: for i being Element of I holds EqR . i = H

for i being set st i in I holds

EqR . i is Relation of (M . i)

proof

then reconsider EqR = EqR as ManySortedRelation of M by MSUALG_4:def 1;
let i be set ; :: thesis: ( i in I implies EqR . i is Relation of (M . i) )

assume i in I ; :: thesis: EqR . i is Relation of (M . i)

then reconsider i9 = i as Element of I ;

EqR . i = EqCl (R . i9) by A1;

hence EqR . i is Relation of (M . i) ; :: thesis: verum

end;assume i in I ; :: thesis: EqR . i is Relation of (M . i)

then reconsider i9 = i as Element of I ;

EqR . i = EqCl (R . i9) by A1;

hence EqR . i is Relation of (M . i) ; :: thesis: verum

for i being set

for R being Relation of (M . i) st i in I & EqR . i = R holds

R is Equivalence_Relation of (M . i)

proof

then reconsider EqR = EqR as Equivalence_Relation of M by MSUALG_4:def 2;
let i be set ; :: thesis: for R being Relation of (M . i) st i in I & EqR . i = R holds

R is Equivalence_Relation of (M . i)

let R1 be Relation of (M . i); :: thesis: ( i in I & EqR . i = R1 implies R1 is Equivalence_Relation of (M . i) )

assume that

A2: i in I and

A3: EqR . i = R1 ; :: thesis: R1 is Equivalence_Relation of (M . i)

reconsider i9 = i as Element of I by A2;

R1 = EqCl (R . i9) by A1, A3;

hence R1 is Equivalence_Relation of (M . i) ; :: thesis: verum

end;R is Equivalence_Relation of (M . i)

let R1 be Relation of (M . i); :: thesis: ( i in I & EqR . i = R1 implies R1 is Equivalence_Relation of (M . i) )

assume that

A2: i in I and

A3: EqR . i = R1 ; :: thesis: R1 is Equivalence_Relation of (M . i)

reconsider i9 = i as Element of I by A2;

R1 = EqCl (R . i9) by A1, A3;

hence R1 is Equivalence_Relation of (M . i) ; :: thesis: verum

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