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₃( Element of D) -> Element of Class RD = EqClass RD,$1;
defpred S₁[ 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

A2: now

let x2, x3, x1 be Element of D; :: thesis: S₁[ EqClass RD,x2, EqClass RD,x3, EqClass RD,x1]
(F /\/ RD) . ((G /\/ RD) . H₃(x2),H₃(x3)),H₃(x1) = (F /\/ RD) . H₃(G . x2,x3),H₃(x1) by Th3
.= H₃(F . (G . x2,x3),x1) by Th3
.= H₃(G . (F . x2,x1),(F . x3,x1)) by A1
.= (G /\/ RD) . H₃(F . x2,x1),H₃(F . x3,x1) by Th3
.= (G /\/ RD) . ((F /\/ RD) . H₃(x2),H₃(x1)),H₃(F . x3,x1) by Th3
.= (G /\/ RD) . ((F /\/ RD) . H₃(x2),H₃(x1)),((F /\/ RD) . H₃(x3),H₃(x1)) by Th3 ;
hence S₁[ EqClass RD,x2, EqClass RD,x3, EqClass RD,x1] ; :: thesis: verum

end;

thus for c2, c3, c1 being Element of Class RD holds S₁[c2,c3,c1] from FILTER_1:sch 3(A2); :: according to BINOP_1:def 19 :: thesis: verum