let D be non empty set ; 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; 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; ( 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)))
; BINOP_1:def 19 F /\/ RD is_right_distributive_wrt G /\/ RD
A2:
now 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;
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)]
;
verum end;
thus
for c2, c3, c1 being Element of Class RD holds S1[c2,c3,c1]
from FILTER_1:sch 3(A2); BINOP_1:def 19 verum