theorem Th20: :: VECTSP_1:24

for F being non empty non degenerated right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for x being Element of F st x <> 0. F holds
(x ") " = x