for SAS being Semi_Affine_Space
for a, o being Element of SAS holds sum (a,o,o) = a by Th64, Def5;