let R be Ring; :: thesis: for a, b being Element of R st a * b = 1. R & ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) holds
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 & ( 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 ) )
assume A1: a * b = 1. R ; :: thesis: ( ex b9 being Element of R st
( a * b9 = 1. R & not b9 = b ) or for x being Element of R holds
( a * x <> 0. R or x = 0. R ) )
assume A2: for b9 being Element of R st a * b9 = 1. R holds
b9 = b ; :: thesis: for x being Element of R holds
( a * x <> 0. R or x = 0. R )
let x be Element of R; :: thesis: ( a * x <> 0. R or x = 0. R )
assume A3: a * x = 0. R ; :: thesis: x = 0. R
a * (b + x) = (a * b) + (a * x) by VECTSP_1:def 7
.= 1. R by A1, A3 ;
then b + x = b by A2;
then b - b = (b + (- b)) + x by RLVECT_1:def 3
.= (0. R) + x by RLVECT_1:5
.= x ;
hence x = 0. R by RLVECT_1:5; :: thesis: verum