let x be Element of L; :: thesis: x is left_invertible
thus ex y being Element of L st y * x = 1. L by Def14; :: according to ALGSTR_0:def 27 :: thesis: verum