let L be non empty multLoopStr ; :: thesis: ( L is left_unital & L is right_unital implies L is unital )
assume A2: ( ( for x being Element of L holds (1. L) * x = x ) & ( for x being Element of L holds x * (1. L) = x ) ) ; :: according to VECTSP_1:def 4,VECTSP_1:def 8 :: thesis: L is unital
take 1. L ; :: according to GROUP_1:def 1 :: thesis: for b₁ being Element of the carrier of L holds
( b₁ * (1. L) = b₁ & (1. L) * b₁ = b₁ )
thus for b₁ being Element of the carrier of L holds
( b₁ * (1. L) = b₁ & (1. L) * b₁ = b₁ ) by A2; :: thesis: verum