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 H3( Element of D) -> Element of Class RD = EqClass (RD,\$1);
defpred S1[ 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:
A2: now :: thesis: for x2, x3, x1 being Element of D holds S1[ EqClass (RD,x2), EqClass (RD,x3), EqClass (RD,x1)]
let x2, x3, x1 be Element of D; :: thesis: S1[ EqClass (RD,x2), EqClass (RD,x3), EqClass (RD,x1)]
(F /\/ RD) . (((G /\/ RD) . (H3(x2),H3(x3))),H3(x1)) = (F /\/ RD) . (H3(G . (x2,x3)),H3(x1)) by Th3
.= H3(F . ((G . (x2,x3)),x1)) by Th3
.= H3(G . ((F . (x2,x1)),(F . (x3,x1)))) by A1
.= (G /\/ RD) . (H3(F . (x2,x1)),H3(F . (x3,x1))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x2),H3(x1))),H3(F . (x3,x1))) by Th3
.= (G /\/ RD) . (((F /\/ RD) . (H3(x2),H3(x1))),((F /\/ RD) . (H3(x3),H3(x1)))) by Th3 ;
hence S1[ EqClass (RD,x2), EqClass (RD,x3), EqClass (RD,x1)] ; :: thesis: verum
end;
thus for c2, c3, c1 being Element of Class RD holds S1[c2,c3,c1] from :: according to BINOP_1:def 19 :: thesis: verum