let L be non empty multLoopStr ; :: thesis: ( L is well-unital implies ( L is left_unital & L is right_unital ) )
assume A1: L is well-unital ; :: thesis: ( L is left_unital & L is right_unital )
hence for x being Element of L holds (1. L) * x = x by Def16; :: according to VECTSP_1:def 8 :: thesis: L is right_unital
thus for x being Element of L holds x * (1. L) = x by A1, Def16; :: according to VECTSP_1:def 4 :: thesis: verum