let D be non empty set ; :: thesis: for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

let RD be Equivalence_Relation of D; :: thesis: for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

let F, G be BinOp of D,RD; :: thesis: ( F is_right_distributive_wrt G implies F /\/ RD is_right_distributive_wrt G /\/ RD )

deffunc H_{3}( Element of D) -> Element of Class RD = EqClass (RD,$1);

defpred S_{1}[ Element of Class RD, Element of Class RD, Element of Class RD] means (F /\/ RD) . (((G /\/ RD) . ($1,$2)),$3) = (G /\/ RD) . (((F /\/ RD) . ($1,$3)),((F /\/ RD) . ($2,$3)));

assume A1: for a, b, d being Element of D holds F . ((G . (a,b)),d) = G . ((F . (a,d)),(F . (b,d))) ; :: according to BINOP_1:def 19 :: thesis: F /\/ RD is_right_distributive_wrt G /\/ RD

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

for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

let RD be Equivalence_Relation of D; :: thesis: for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

let F, G be BinOp of D,RD; :: thesis: ( F is_right_distributive_wrt G implies F /\/ RD is_right_distributive_wrt G /\/ RD )

deffunc H

defpred S

assume A1: for a, b, d being Element of D holds F . ((G . (a,b)),d) = G . ((F . (a,d)),(F . (b,d))) ; :: according to BINOP_1:def 19 :: thesis: F /\/ RD is_right_distributive_wrt G /\/ RD

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

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

(F /\/ RD) . (((G /\/ RD) . (H_{3}(x2),H_{3}(x3))),H_{3}(x1)) =
(F /\/ RD) . (H_{3}(G . (x2,x3)),H_{3}(x1))
by Th3

.= H_{3}(F . ((G . (x2,x3)),x1))
by Th3

.= H_{3}(G . ((F . (x2,x1)),(F . (x3,x1))))
by A1

.= (G /\/ RD) . (H_{3}(F . (x2,x1)),H_{3}(F . (x3,x1)))
by Th3

.= (G /\/ RD) . (((F /\/ RD) . (H_{3}(x2),H_{3}(x1))),H_{3}(F . (x3,x1)))
by Th3

.= (G /\/ RD) . (((F /\/ RD) . (H_{3}(x2),H_{3}(x1))),((F /\/ RD) . (H_{3}(x3),H_{3}(x1))))
by Th3
;

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

end;(F /\/ RD) . (((G /\/ RD) . (H

.= H

.= H

.= (G /\/ RD) . (H

.= (G /\/ RD) . (((F /\/ RD) . (H

.= (G /\/ RD) . (((F /\/ RD) . (H

hence S