theorem :: VECTSP_1:27

for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F st a - b = 0. F holds
a = b by Th15;