let IT be Element of F; :: thesis: ( IT = x " iff IT * x = 1. F )
A2: x is left_invertible by A1, ALGSTR_0:def 39;
then consider x1 being Element of F such that
A3: x1 * x = 1. F ;
x is right_mult-cancelable

proof

let y, z be Element of F; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )
assume A4: y * x = z * x ; :: thesis: y = z
thus y = y * (1. F)
.= (z * x) * x1 by A3, A4, GROUP_1:def 3
.= z * (1. F) by A3, GROUP_1:def 3
.= z ; :: thesis: verum

end;

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