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)

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)

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

then reconsider U3 = EqR1 (/\) EqR2 as ManySortedRelation of M by MSUALG_4:def 1;
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 A1, MSUALG_4:def 1;

(EqR1 (/\) EqR2) . i = U19 /\ U29 by A1, PBOOLE:def 5;

hence (EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i) ; :: thesis: verum

end;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 A1, MSUALG_4:def 1;

(EqR1 (/\) EqR2) . i = U19 /\ U29 by A1, PBOOLE:def 5;

hence (EqR1 (/\) EqR2) . i is Relation of (M . i),(M . i) ; :: thesis: verum

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

hence
EqR1 (/\) EqR2 is Equivalence_Relation of M
by MSUALG_4:def 2; :: thesis: verum
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 A2, MSUALG_4:def 1;

reconsider U29 = U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

reconsider U19 = EqR1 . i as Relation of (M . i) by A2, MSUALG_4:def 1;

reconsider U19 = U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

U19 /\ U29 is Equivalence_Relation of (M . i) ;

hence R is Equivalence_Relation of (M . i) by A2, A3, PBOOLE:def 5; :: thesis: verum

end;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 A2, MSUALG_4:def 1;

reconsider U29 = U29 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

reconsider U19 = EqR1 . i as Relation of (M . i) by A2, MSUALG_4:def 1;

reconsider U19 = U19 as Equivalence_Relation of (M . i) by A2, MSUALG_4:def 2;

U19 /\ U29 is Equivalence_Relation of (M . i) ;

hence R is Equivalence_Relation of (M . i) by A2, A3, PBOOLE:def 5; :: thesis: verum