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 by ALGSTR_0:def 27;
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) by Def16
.= (z * x) * x1 by A3, A4, GROUP_1:def 4
.= z * (1. F) by A3, GROUP_1:def 4
.= z by Def16 ; :: thesis: verum

end;

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