thus
( IT is almost_left_invertible implies for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT ) by ALGSTR_0:def 27; :: thesis: ( ( for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT ) implies IT is almost_left_invertible )

assume A1: for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT ; :: thesis: IT is almost_left_invertible

let x be Element of IT; :: according to ALGSTR_0:def 38 :: thesis: ( x = 0. IT or x is left_invertible )

assume x <> 0. IT ; :: thesis: x is left_invertible

hence ex y being Element of IT st y * x = 1. IT by A1; :: according to ALGSTR_0:def 27 :: thesis: verum

ex y being Element of IT st y * x = 1. IT ) by ALGSTR_0:def 27; :: thesis: ( ( for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT ) implies IT is almost_left_invertible )

assume A1: for x being Element of IT st x <> 0. IT holds

ex y being Element of IT st y * x = 1. IT ; :: thesis: IT is almost_left_invertible

let x be Element of IT; :: according to ALGSTR_0:def 38 :: thesis: ( x = 0. IT or x is left_invertible )

assume x <> 0. IT ; :: thesis: x is left_invertible

hence ex y being Element of IT st y * x = 1. IT by A1; :: according to ALGSTR_0:def 27 :: thesis: verum