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 )

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

hence
L is domRing-like
by VECTSP_2:def 1; :: thesis: verum
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 )

end;assume A2: x * y = 0. L ; :: thesis: ( x = 0. L or y = 0. L )

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

hence
( x = 0. L or y = 0. L )
; :: thesis: verumassume 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;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