let L be non empty right_add-cancelable right-distributive well-unital associative 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 :: thesis: for x, y being Element of L holds
( not x * y = 0. L or x = 0. L or y = 0. L )
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;
z * (0. L) = (1. L) * y by A2, A3, GROUP_1:def 3
.= y ;
hence y = 0. L by Lm1; :: thesis: verum
end;
end;
hence L is domRing-like by VECTSP_2:def 1; :: thesis: verum