let SAS be Semi_Affine_Space; :: thesis: for a, o being Element of SAS st sum (a,a,o) = o holds
a = o
let a, o be Element of SAS; :: thesis: ( sum (a,a,o) = o implies a = o )
assume sum (a,a,o) = o ; :: thesis: a = o
then congr o,a,a,o by Def5;
hence a = o by Th56; :: thesis: verum