let A be non empty set ; for o, o9 being BinOp of A st o9 is commutative 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) )
let o, o9 be BinOp of A; ( o9 is commutative implies ( 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) ) )
assume A1:
o9 is commutative
; ( 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) )
( ( 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) ) ) iff for a, b, c being Element of A holds o9 . a,(o . b,c) = o . (o9 . a,b),(o9 . a,c) )
proof
thus
( ( 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 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 . a,(o . b,c) = o . (o9 . a,b),(o9 . a,c) ) 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) ) )
assume A2:
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 . a,(o . b,c) = o . (o9 . a,b),(o9 . a,c) & o9 . (o . a,b),c = o . (o9 . a,c),(o9 . b,c) )
let a,
b,
c be
Element of
A;
( 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 . a,
(o . b,c) = o . (o9 . a,b),
(o9 . a,c)
by A2;
o9 . (o . a,b),c = o . (o9 . a,c),(o9 . b,c)
thus o9 . (o . a,b),
c =
o9 . c,
(o . a,b)
by A1, Def2
.=
o . (o9 . c,a),
(o9 . c,b)
by A2
.=
o . (o9 . a,c),
(o9 . c,b)
by A1, Def2
.=
o . (o9 . a,c),
(o9 . b,c)
by A1, Def2
;
verum
end;
hence
( 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) )
by Th23; verum