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