let I be non empty set ; :: thesis: for M being ManySortedSet of I
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
let M be ManySortedSet of I; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 /\ EqR2 is Equivalence_Relation of M
for i being set st i in I holds
(EqR1 /\ EqR2) . i is Relation of M . i,M . i

proof

let i be set ; :: thesis: ( i in I implies (EqR1 /\ EqR2) . i is Relation of M . i,M . i )
assume A1: i in I ; :: thesis: (EqR1 /\ EqR2) . i is Relation of M . i,M . i
then reconsider U1' = EqR1 . i as Relation of M . i,M . i by MSUALG_4:def 2;
reconsider U2' = EqR2 . i as Relation of M . i,M . i by A1, MSUALG_4:def 2;
(EqR1 /\ EqR2) . i = U1' /\ U2' by A1, PBOOLE:def 8;
hence (EqR1 /\ EqR2) . i is Relation of M . i,M . i ; :: thesis: verum

end;

then reconsider U3 = EqR1 /\ EqR2 as ManySortedRelation of M by MSUALG_4:def 2;
for i being set
for R being Relation of M . i st i in I & U3 . 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 & U3 . i = R holds
R is Equivalence_Relation of M . i
let R be Relation of M . i; :: thesis: ( i in I & U3 . i = R implies R is Equivalence_Relation of M . i )
assume A2: ( i in I & U3 . i = R ) ; :: thesis: R is Equivalence_Relation of M . i
then reconsider U1' = EqR1 . i as Relation of M . i by MSUALG_4:def 2;
reconsider U1' = U1' as Equivalence_Relation of M . i by A2, MSUALG_4:def 3;
reconsider U2' = EqR2 . i as Relation of M . i by A2, MSUALG_4:def 2;
reconsider U2' = U2' as Equivalence_Relation of M . i by A2, MSUALG_4:def 3;
U1' /\ U2' is Equivalence_Relation of M . i ;
hence R is Equivalence_Relation of M . i by A2, PBOOLE:def 8; :: thesis: verum

end;

hence EqR1 /\ EqR2 is Equivalence_Relation of M by MSUALG_4:def 3; :: thesis: verum