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, sum a,o,o & congr o,a,o,a ) by Def5, Th84;
hence sum a,o,o = a by Th81; :: thesis: verum