let R be commutative domRing-like Ring; :: thesis: for a, b being Element of R st a <> 0. R & a * b = a holds
b = 1. R
let A, B be Element of R; :: thesis: ( A <> 0. R & A * B = A implies B = 1. R )
assume that
A1: A <> 0. R and
A2: A * B = A ; :: thesis: B = 1. R
set A1 = A / A;
( A / A = 1. R & (A * B) / A = (A / A) * B ) by A1, A2, Th9, Th11;
hence B = 1. R by A2; :: thesis: verum