let D be non empty set ; :: thesis: for RD being Equivalence_Relation of D
for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
let RD be Equivalence_Relation of D; :: thesis: for F being BinOp of D,RD st F is commutative holds
F /\/ RD is commutative
let F be BinOp of D,RD; :: thesis: ( F is commutative implies F /\/ RD is commutative )
assume A1:
for a, b being Element of D holds F . a,b = F . b,a
; :: according to BINOP_1:def 13 :: thesis: F /\/ RD is commutative
defpred S1[ Element of Class RD, Element of Class RD] means (F /\/ RD) . $1,$2 = (F /\/ RD) . $2,$1;
A2:
now let x1,
x2 be
Element of
D;
:: thesis: S1[ EqClass RD,x1, EqClass RD,x2]thus
S1[
EqClass RD,
x1,
EqClass RD,
x2]
:: thesis: verumproof
thus (F /\/ RD) . (EqClass RD,x1),
(EqClass RD,x2) =
Class RD,
(F . x1,x2)
by Th3
.=
Class RD,
(F . x2,x1)
by A1
.=
(F /\/ RD) . (EqClass RD,x2),
(EqClass RD,x1)
by Th3
;
:: thesis: verum
end; end;
thus
for c1, c2 being Element of Class RD holds S1[c1,c2]
from FILTER_1:sch 2(A2); :: according to BINOP_1:def 13 :: thesis: verum