let S be non empty doubleLoopStr ; :: thesis: ( S is trivial implies ( S is well-unital & S is right-distributive ) )
assume A2: S is trivial ; :: thesis: ( S is well-unital & S is right-distributive )
thus for x being Element of S holds
( x * (1. S) = x & (1. S) * x = x ) by A2, STRUCT_0:def 10; :: according to VECTSP_1:def 16 :: thesis: S is right-distributive
let x, y, z be Element of S; :: according to VECTSP_1:def 11 :: thesis: x * (y + z) = (x * y) + (x * z)
thus x * (y + z) = (x * y) + (x * z) by A2, STRUCT_0:def 10; :: thesis: verum