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