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