theorem :: MIDSP_2:11

for G being non empty Abelian add-associative addLoopStr
for x, y being Element of G holds Double (x + y) = (Double x) + (Double y) by Th10;