let IT be Element of L; :: thesis: ( IT = x " iff IT * x = 1. L )

ex x1 being Element of L st x1 * x = 1. L by A1, Def8;

then A2: x is left_invertible ;

x is right_mult-cancelable by A1, ALGSTR_0:def 37;

hence ( IT = x " iff IT * x = 1. L ) by A2, ALGSTR_0:def 30; :: thesis: verum

ex x1 being Element of L st x1 * x = 1. L by A1, Def8;

then A2: x is left_invertible ;

x is right_mult-cancelable by A1, ALGSTR_0:def 37;

hence ( IT = x " iff IT * x = 1. L ) by A2, ALGSTR_0:def 30; :: thesis: verum