let M be non empty Abelian commutative doubleLoopStr ; :: thesis: ( M is left-distributive implies M is right-distributive )
assume A4: M is left-distributive ; :: thesis: M is right-distributive
let x, y, z be Element of M; :: according to VECTSP_1:def 2 :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) by A4; :: thesis: verum