let R be Ring; :: thesis: for a, b being Element of R st a * b = 1. R & a is invertible holds
for b9 being Element of R st a * b9 = 1. R holds
b9 = b
let a, b be Element of R; :: thesis: ( a * b = 1. R & a is invertible implies for b9 being Element of R st a * b9 = 1. R holds
b9 = b )
assume A1: a * b = 1. R ; :: thesis: ( not a is invertible or for b9 being Element of R st a * b9 = 1. R holds
b9 = b )
assume A2: a is invertible ; :: thesis: for b9 being Element of R st a * b9 = 1. R holds
b9 = b
let b9 be Element of R; :: thesis: ( a * b9 = 1. R implies b9 = b )
assume A3: a * b9 = 1. R ; :: thesis: b9 = b
consider c being Element of R such that
A4: c * a = 1. R by A2, ALGSTR_0:def 27;
A5: b9 = (1. R) * b9
.= c * (a * b9) by A4, GROUP_1:def 3
.= c by A3 ;
thus b = (1. R) * b
.= c * (1. R) by A1, A4, GROUP_1:def 3
.= b9 by A5 ; :: thesis: verum