let L be non empty right_complementable right-distributive well-unital add-associative right_zeroed associative doubleLoopStr ; :: thesis: ( L is almost_left_invertible implies L is domRing-like )
assume A1: L is almost_left_invertible ; :: thesis: L is domRing-like
for x, y being Element of L holds
( not x * y = 0. L or x = 0. L or y = 0. L )

proof

let x, y be Element of L; :: thesis: ( not x * y = 0. L or x = 0. L or y = 0. L )
assume A2: x * y = 0. L ; :: thesis: ( x = 0. L or y = 0. L )

now :: thesis: ( x <> 0. L implies not y <> 0. L )

assume that
A3: x <> 0. L and
A4: y <> 0. L ; :: thesis: contradiction
consider xx being Element of L such that
A5: xx * x = 1. L by A1, A3;
y = (1. L) * y
.= xx * (x * y) by A5, GROUP_1:def 3
.= 0. L by A2 ;
hence contradiction by A4; :: thesis: verum

end;

hence ( x = 0. L or y = 0. L ) ; :: thesis: verum

end;

hence L is domRing-like by VECTSP_2:def 1; :: thesis: verum