theorem Th17: :: MIDSP_2:17

for G being non empty right_complementable Fanoian Abelian add-associative right_zeroed addLoopStr
for x, y being Element of G st Double x = Double y holds
x = y