for F being non degenerated almost_left_invertible Ring
for x being Scalar of F
for V being non empty right_complementable add-associative right_zeroed RightMod-like RightModStr over F
for v being Vector of V st x <> 0. F holds
(v * x) * (x ") = v