let L be non empty multLoopStr ; :: thesis: ( L is well-unital implies 1. L = 1_ L )
assume L is well-unital ; :: thesis: 1. L = 1_ L
then ( ( for h being Element of L holds
( h * (1. L) = h & (1. L) * h = h ) ) & L is unital ) ;
hence 1. L = 1_ L by GROUP_1:def 4; :: thesis: verum