let x be Element of K; :: thesis: ( not x is zero implies x is left_invertible )
assume not x is zero ; :: thesis: x is left_invertible
then x <> 0. K ;
hence x is left_invertible by ALGSTR_0:def 39; :: thesis: verum