let Y be non empty set ; :: thesis: for R, S being Equivalence_Relation of Y st R * S = S * R holds

R * S is Equivalence_Relation of Y

let R, S be Equivalence_Relation of Y; :: thesis: ( R * S = S * R implies R * S is Equivalence_Relation of Y )

assume A1: R * S = S * R ; :: thesis: R * S is Equivalence_Relation of Y

A2: field S = Y by ORDERS_1:12;

then A3: S is_reflexive_in Y by RELAT_2:def 9;

A4: field R = Y by ORDERS_1:12;

then R is_reflexive_in Y by RELAT_2:def 9;

then R * S is_reflexive_in Y by A3, Th7;

then A5: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:13;

A6: R * S is_symmetric_in Y

(R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:36

.= (R * (R * S)) * S by A1, RELAT_1:36

.= ((R * R) * S) * S by RELAT_1:36

.= (R * R) * (S * S) by RELAT_1:36 ;

then (R * S) * (R * S) c= R * S by A14, RELAT_1:31;

hence R * S is Equivalence_Relation of Y by A5, A6, PARTFUN1:def 2, RELAT_2:27, RELAT_2:def 11; :: thesis: verum

R * S is Equivalence_Relation of Y

let R, S be Equivalence_Relation of Y; :: thesis: ( R * S = S * R implies R * S is Equivalence_Relation of Y )

assume A1: R * S = S * R ; :: thesis: R * S is Equivalence_Relation of Y

A2: field S = Y by ORDERS_1:12;

then A3: S is_reflexive_in Y by RELAT_2:def 9;

A4: field R = Y by ORDERS_1:12;

then R is_reflexive_in Y by RELAT_2:def 9;

then R * S is_reflexive_in Y by A3, Th7;

then A5: ( field (R * S) = Y & dom (R * S) = Y ) by ORDERS_1:13;

A6: R * S is_symmetric_in Y

proof

A14:
( R * R c= R & S * S c= S )
by RELAT_2:27;
A7:
S is_symmetric_in Y
by A2, RELAT_2:def 11;

let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in Y or not y in Y or not [x,y] in R * S or [y,x] in R * S )

assume that

A8: x in Y and

A9: y in Y ; :: thesis: ( not [x,y] in R * S or [y,x] in R * S )

assume [x,y] in R * S ; :: thesis: [y,x] in R * S

then consider z being object such that

A10: [x,z] in R and

A11: [z,y] in S by RELAT_1:def 8;

z in field S by A11, RELAT_1:15;

then A12: [y,z] in S by A2, A7, A9, A11;

A13: R is_symmetric_in Y by A4, RELAT_2:def 11;

z in field R by A10, RELAT_1:15;

then [z,x] in R by A4, A13, A8, A10;

hence [y,x] in R * S by A1, A12, RELAT_1:def 8; :: thesis: verum

end;let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in Y or not y in Y or not [x,y] in R * S or [y,x] in R * S )

assume that

A8: x in Y and

A9: y in Y ; :: thesis: ( not [x,y] in R * S or [y,x] in R * S )

assume [x,y] in R * S ; :: thesis: [y,x] in R * S

then consider z being object such that

A10: [x,z] in R and

A11: [z,y] in S by RELAT_1:def 8;

z in field S by A11, RELAT_1:15;

then A12: [y,z] in S by A2, A7, A9, A11;

A13: R is_symmetric_in Y by A4, RELAT_2:def 11;

z in field R by A10, RELAT_1:15;

then [z,x] in R by A4, A13, A8, A10;

hence [y,x] in R * S by A1, A12, RELAT_1:def 8; :: thesis: verum

(R * S) * (R * S) = ((R * S) * R) * S by RELAT_1:36

.= (R * (R * S)) * S by A1, RELAT_1:36

.= ((R * R) * S) * S by RELAT_1:36

.= (R * R) * (S * S) by RELAT_1:36 ;

then (R * S) * (R * S) c= R * S by A14, RELAT_1:31;

hence R * S is Equivalence_Relation of Y by A5, A6, PARTFUN1:def 2, RELAT_2:27, RELAT_2:def 11; :: thesis: verum