let SAS be Semi_Affine_Space; :: thesis: for a, o being Element of SAS holds sum a,o,o = a
let a, o be Element of SAS; :: thesis: sum a,o,o = a
congr o,a,o,a by Th84;
hence sum a,o,o = a by Def5; :: thesis: verum