let A be set ; for o, o9 being BinOp of A holds
( o9 is_distributive_wrt o iff for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
let o, o9 be BinOp of A; ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
thus
( o9 is_distributive_wrt o implies for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
( ( for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ) implies o9 is_distributive_wrt o )proof
assume
(
o9 is_left_distributive_wrt o &
o9 is_right_distributive_wrt o )
;
BINOP_1:def 11 for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
hence
for
a,
b,
c being
Element of
A holds
(
o9 . (
a,
(o . (b,c)))
= o . (
(o9 . (a,b)),
(o9 . (a,c))) &
o9 . (
(o . (a,b)),
c)
= o . (
(o9 . (a,c)),
(o9 . (b,c))) )
;
verum
end;
assume
for a, b, c being Element of A holds
( o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )
; o9 is_distributive_wrt o
hence
( ( for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c))) ) & ( for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
; BINOP_1:def 9,BINOP_1:def 10,BINOP_1:def 11 verum