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

proof

let i be set ; :: thesis: ( i in I implies (id M) . i is Relation of M . i )
assume i in I ; :: thesis: (id M) . i is Relation of M . i
then (id M) . i = id (M . i) by MSUALG_3:def 1;
hence (id M) . i is Relation of M . i ; :: thesis: verum

end;

then reconsider J = id 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 = id (M . i) by MSUALG_3:def 1;
hence R is Equivalence_Relation of M . i by A1, EQREL_1:6; :: thesis: verum

end;

hence id M is Equivalence_Relation of M by MSUALG_4:def 3; :: thesis: verum