let R be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis: ( R is domRing-like & R is right_unital )
thus R is domRing-like :: thesis: R is right_unital
proof
let x, y be Element of R; :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. R or x = 0. R or y = 0. R )
assume that
A1: x * y = 0. R and
A2: x <> 0. R ; :: thesis: y = 0. R
x * y = x * (0. R) by A1;
hence y = 0. R by A2, VECTSP_1:5; :: thesis: verum
end;
let x be Element of R; :: according to VECTSP_1:def 4 :: thesis: x * (1. R) = x
thus x * (1. R) = x ; :: thesis: verum