let I be non empty set ; :: thesis: for M being ManySortedSet of
for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 /\ EqR2 is Equivalence_Relation of M
let M be ManySortedSet of ; :: 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