let L be non empty right_add-cancelable associative commutative right-distributive well-unital left_zeroed doubleLoopStr ; :: thesis: ( L is almost_left_invertible implies L is domRing-like )
assume A1: L is almost_left_invertible ; :: thesis: L is domRing-like

now

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 )
thus ( x = 0. L or y = 0. L ) :: thesis: verum

proof

assume x <> 0. L ; :: thesis: y = 0. L
then consider z being Element of L such that
A3: z * x = 1. L by A1, VECTSP_1:def 20;
z * (0. L) = (1. L) * y by A2, A3, GROUP_1:def 4
.= y by VECTSP_1:def 19 ;
hence y = 0. L by Lm1; :: thesis: verum

end;

end;

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