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 ) :: 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 )

proof

assume A1: IT is almost_left_invertible ; :: thesis: for x being Element of IT st x <> 0. IT holds
ex y being Element of IT st y * x = 1. IT
let x be Element of IT; :: thesis: ( x <> 0. IT implies ex y being Element of IT st y * x = 1. IT )
assume x <> 0. IT ; :: thesis: ex y being Element of IT st y * x = 1. IT
then x is left_invertible by A1, ALGSTR_0:def 39;
hence ex y being Element of IT st y * x = 1. IT by ALGSTR_0:def 27; :: thesis: verum

end;

assume A2: 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 39 :: 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 A2; :: according to ALGSTR_0:def 27 :: thesis: verum