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 )

defpred S_{1}[ 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);

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 3 :: thesis: F /\/ RD is associative

_{1}[c1,c2,c3]
from FILTER_1:sch 3(A2); :: according to BINOP_1:def 3 :: thesis: verum

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 )

defpred S

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 3 :: thesis: F /\/ RD is associative

A2: now :: thesis: for x1, x2, x3 being Element of D holds S_{1}[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)]

thus
for c1, c2, c3 being Element of Class RD holds Slet x1, x2, x3 be Element of D; :: thesis: S_{1}[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)]

(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 ;

hence S_{1}[ EqClass (RD,x1), EqClass (RD,x2), EqClass (RD,x3)]
; :: thesis: verum

end;(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 ;

hence S