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 U19 = EqR1 . i as Relation of (M . i),(M . i) by MSUALG_4:def 1;
reconsider U29 = EqR2 . i as Relation of (M . i),(M . i) by ;
(EqR1 (/\) EqR2) . i = U19 /\ U29 by ;
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 1;
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 that
A2: i in I and
A3: U3 . i = R ; :: thesis: R is Equivalence_Relation of (M . i)
reconsider U29 = EqR2 . i as Relation of (M . i) by ;
reconsider U29 = U29 as Equivalence_Relation of (M . i) by ;
reconsider U19 = EqR1 . i as Relation of (M . i) by ;
reconsider U19 = U19 as Equivalence_Relation of (M . i) by ;
U19 /\ U29 is Equivalence_Relation of (M . i) ;
hence R is Equivalence_Relation of (M . i) by ; :: thesis: verum
end;
hence EqR1 (/\) EqR2 is Equivalence_Relation of M by MSUALG_4:def 2; :: thesis: verum