let Y be non empty set ; 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; ( R * S = S * R implies R * S is Equivalence_Relation of Y )
assume A1:
R * S = S * R
; 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
A7:
S is_symmetric_in Y
by A2, RELAT_2:def 11;
let x,
y be
object ;
RELAT_2:def 3 ( 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
;
( not [x,y] in R * S or [y,x] in R * S )
assume
[x,y] in R * S
;
[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;
verum
end;
A14:
( R * R c= R & S * S c= S )
by RELAT_2:27;
(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; verum