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 for x being Element of R holds
( a * x <> 0. R or x = 0. R ) )
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 for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) )
assume A1: a * b = 1. R ; :: thesis: ( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff for x being Element of R holds
( a * x <> 0. R or x = 0. R ) )
thus ( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) implies for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) by A1, Lm4; :: thesis: ( ( for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) implies for b9 being Element of R st a * b9 = 1. R holds
b9 = b )
assume for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ; :: thesis: for b9 being Element of R st a * b9 = 1. R holds
b9 = b
then a is invertible by A1, Lm5;
hence for b9 being Element of R st a * b9 = 1. R holds
b9 = b by A1, Lm6; :: thesis: verum