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, Def24;
then A2: x is left_invertible by ALGSTR_0:def 27;
x is right_mult-cancelable by A1, ALGSTR_0:def 37;
hence ( IT = x " iff IT * x = 1. L ) by A2, ALGSTR_0:def 35; :: thesis: verum