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_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
let RD be Equivalence_Relation of D; :: thesis: for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds
F /\/ RD is_left_distributive_wrt G /\/ RD
let F, G be BinOp of D,RD; :: thesis: ( F is_left_distributive_wrt G implies F /\/ RD is_left_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) . $1,((G /\/ RD) . $2,$3) = (G /\/ RD) . ((F /\/ RD) . $1,$2),((F /\/ RD) . $1,$3);
assume A1: for d, a, b being Element of D holds F . d,(G . a,b) = G . (F . d,a),(F . d,b) ; :: according to BINOP_1:def 18 :: thesis: F /\/ RD is_left_distributive_wrt G /\/ RD

A2: now

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

end;

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