theorem :: SEMI_AF1:77

for SAS being Semi_Affine_Space
for a, b, c, o being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o)