let R be non empty doubleLoopStr ; :: thesis: ( R is commutative & R is left-distributive implies R is distributive )
assume that
A3: R is commutative and
A4: R is left-distributive ; :: thesis: R is distributive
let x, y, z be Element of R; :: according to VECTSP_1:def 7 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = (y + z) * x by A3, GROUP_1:def 12
.= (y * x) + (z * x) by A4
.= (x * y) + (z * x) by A3, GROUP_1:def 12
.= (x * y) + (x * z) by A3, GROUP_1:def 12 ; :: thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (y * x) + (z * x) by A4; :: thesis: verum