let SAS be Semi_Affine_Space; :: thesis: for o being Element of SAS holds opposite (o,o) = o
let o be Element of SAS; :: thesis: opposite (o,o) = o
sum (o,(opposite (o,o)),o) = o by Def6;
then sum ((opposite (o,o)),o,o) = o by Th78;
hence opposite (o,o) = o by Th75; :: thesis: verum