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