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

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