theorem Th1: :: IDEAL_1:1

for V being non empty add-associative right_zeroed left_zeroed addLoopStr
for v, u being Element of V holds Sum <*v,u*> = v + u