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