let I be non empty set ; :: thesis: for M being ManySortedSet of holds [|M,M|] is Equivalence_Relation of M
let M be ManySortedSet of ; :: thesis: [|M,M|] is Equivalence_Relation of M
set J = [|M,M|];
for i being set st i in I holds
[|M,M|] . i is Relation of (M . i)

proof

let i be set ; :: thesis: ( i in I implies [|M,M|] . i is Relation of (M . i) )
assume i in I ; :: thesis: [|M,M|] . i is Relation of (M . i)
then [|M,M|] . i c= [:(M . i),(M . i):] by PBOOLE:def 21;
hence [|M,M|] . i is Relation of (M . i) ; :: thesis: verum

end;

then reconsider J = [|M,M|] as ManySortedRelation of M by MSUALG_4:def 2;
for i being set
for R being Relation of (M . i) st i in I & J . 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 & J . i = R holds
R is Equivalence_Relation of (M . i)
let R be Relation of (M . i); :: thesis: ( i in I & J . i = R implies R is Equivalence_Relation of (M . i) )
assume A1: ( i in I & J . i = R ) ; :: thesis: R is Equivalence_Relation of (M . i)
then J . i = [:(M . i),(M . i):] by PBOOLE:def 21
.= nabla (M . i) by EQREL_1:def 1 ;
hence R is Equivalence_Relation of (M . i) by A1, EQREL_1:7; :: thesis: verum

end;

hence [|M,M|] is Equivalence_Relation of M by MSUALG_4:def 3; :: thesis: verum