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 A1: ( A <> 0. R & A * B = A ) ; :: thesis: B = 1. R
set A1 = A / A;
A2: A / A = 1. R by A1, Th9;
(A * B) / A = (A / A) * B by A1, Th11;
hence B = 1. R by A1, A2, VECTSP_1:def 19; :: thesis: verum