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 ,

proof

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

proof

let i be set ; :: thesis: for R being Relation of st i in I & U3 . i = R holds
R is Equivalence_Relation of
let R be Relation of ; :: thesis: ( i in I & U3 . i = R implies R is Equivalence_Relation of )
assume that
A2: i in I and
A3: U3 . i = R ; :: thesis: R is Equivalence_Relation of
reconsider U2' = EqR2 . i as Relation of by A2, MSUALG_4:def 2;
reconsider U2' = U2' as Equivalence_Relation of by A2, MSUALG_4:def 3;
reconsider U1' = EqR1 . i as Relation of by A2, MSUALG_4:def 2;
reconsider U1' = U1' as Equivalence_Relation of by A2, MSUALG_4:def 3;
U1' /\ U2' is Equivalence_Relation of ;
hence R is Equivalence_Relation of by A2, A3, PBOOLE:def 8; :: thesis: verum

end;

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