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