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