let IT be Element of L; :: thesis: ( IT = x " iff IT * x = 1. L )
consider x1 being Element of L such that
A2: x1 * x = 1. L by A1, Def24;
A3: x is left_invertible by A2, ALGSTR_0:def 27;
x is right_mult-cancelable by A1, ALGSTR_0:def 37;
hence ( IT = x " iff IT * x = 1. L ) by A3, ALGSTR_0:def 35; :: thesis: verum