theorem Th3: :: BINOM:3

for L being non empty left_zeroed addLoopStr
for a being Element of L holds Sum <*a*> = a