let R be Ring; :: thesis: for a, b being Element of R st a * b = 1. R holds
( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff a is invertible )
let a, b be Element of R; :: thesis: ( a * b = 1. R implies ( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff a is invertible ) )
assume A1: a * b = 1. R ; :: thesis: ( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff a is invertible )

hereby :: thesis: ( a is invertible implies for b9 being Element of R st a * b9 = 1. R holds
b9 = b )

assume for b9 being Element of R st a * b9 = 1. R holds
b9 = b ; :: thesis: a is invertible
then for x being Element of R holds
( a * x <> 0. R or x = 0. R ) by A1, Lm4;
hence a is invertible by A1, Lm5; :: thesis: verum

end;

assume a is invertible ; :: thesis: for b9 being Element of R st a * b9 = 1. R holds
b9 = b
hence for b9 being Element of R st a * b9 = 1. R holds
b9 = b by A1, Lm6; :: thesis: verum