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 for h being Element of L holds
( h * (1. L) = h & (1. L) * h = h ) by VECTSP_1:def 6;
hence 1. L = 1_ L by A1, GROUP_1:def 4; :: thesis: verum