let L be non empty multLoopStr ; :: thesis: ( L is well-unital implies L is unital )
assume A1: L is well-unital ; :: thesis: L is unital
take 1. L ; :: according to GROUP_1:def 2 :: 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 A1, Def16; :: thesis: verum