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