let D be non empty doubleLoopStr ; :: thesis: ( D is left-distributive & D is right-distributive implies D is distributive )
assume ( ( for a, b, c being Element of D holds (b + c) * a = (b * a) + (c * a) ) & ( for a, b, c being Element of D holds a * (b + c) = (a * b) + (a * c) ) ) ; :: according to VECTSP_1:def 2,VECTSP_1:def 3 :: thesis: D is distributive
hence for x, y, z being Element of D holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ; :: according to VECTSP_1:def 7 :: thesis: verum