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

proof

take y ; :: according to ALGSTR_0:def 28 :: thesis: x * y = 1. SF
thus x * y = 1. SF by A3, Th7; :: thesis: verum

end;

then consider x1 being Element of SF such that
A4: x * x1 = 1. SF ;
x is right_mult-cancelable

proof

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

end;

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