theorem LX1: :: RING_4:16

for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr
for a being Element of L holds a | L = a * (1_. L)