let R be Ring; :: thesis: for a, b being Element of R st a * b = 1. R & ( for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) holds
a is invertible
let a, b be Element of R; :: thesis: ( a * b = 1. R & ( for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) implies a is invertible )
assume A1: a * b = 1. R ; :: thesis: ( ex x being Element of R st
( not a * x <> 0. R & not x = 0. R ) or a is invertible )
assume A2: for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ; :: thesis: a is invertible
( a is right_invertible & a is left_invertible )

proof

thus a is right_invertible by A1, ALGSTR_0:def 28; :: thesis: a is left_invertible
set x = (1. R) - (b * a);
a * ((1. R) - (b * a)) = (a * (1. R)) - (a * (b * a)) by VECTSP_1:11
.= a - ((a * b) * a) by GROUP_1:def 3
.= 0. R by A1, RLVECT_1:5 ;
then (1. R) - (b * a) = 0. R by A2;
then b * a = ((1. R) - (b * a)) + (b * a)
.= (1. R) + ((- (b * a)) + (b * a)) by RLVECT_1:def 3
.= (1. R) + (0. R) by RLVECT_1:5
.= 1. R ;
hence a is left_invertible by ALGSTR_0:def 27; :: thesis: verum

end;

hence a is invertible ; :: thesis: verum