let A be non empty set ; :: thesis: 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 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) )

let o, o9 be BinOp of A; :: thesis: ( o9 is commutative implies ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
assume A1: o9 is commutative ; :: thesis: ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds 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))) ) ) iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,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 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) ; :: thesis: ( ( for a, b, c being Element of A holds 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))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )

assume A2: for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ; :: thesis: 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; :: thesis: ( 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))) = o9 . ((o . (b,c)),a) by A1
.= o . ((o9 . (b,a)),(o9 . (c,a))) by A2
.= o . ((o9 . (a,b)),(o9 . (c,a))) by A1
.= o . ((o9 . (a,b)),(o9 . (a,c))) by A1 ; :: thesis: o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)))
thus o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) by A2; :: thesis: verum
end;
hence ( o9 is_distributive_wrt o iff for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) by Th11; :: thesis: verum