let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: ( L is domRing-like implies L is almost_right_cancelable )
assume A3: L is domRing-like ; :: thesis: L is almost_right_cancelable
let x be Element of L; :: according to ALGSTR_0:def 36 :: thesis: ( x = 0. L or x is right_mult-cancelable )
assume A4: x <> 0. L ; :: thesis: x is right_mult-cancelable
let y, z be Element of L; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )
assume y * x = z * x ; :: thesis: y = z
then (y * x) - (z * x) = 0. L by RLVECT_1:15;
then (y - z) * x = 0. L by VECTSP_1:13;
then y - z = 0. L by A4, A3;
hence y = z by RLVECT_1:21; :: thesis: verum