let SAS be Semi_Affine_Space; :: thesis: for a, b, o, c being Element of SAS holds sum (sum a,b,o),c,o = sum a,(sum b,c,o),o
let a, b, o, c be Element of SAS; :: thesis: sum (sum a,b,o),c,o = sum a,(sum b,c,o),o
( congr o,a,b, sum a,b,o & congr o,a, sum b,c,o, sum a,(sum b,c,o),o ) by Def5;
then A1: congr b, sum a,b,o, sum b,c,o, sum a,(sum b,c,o),o by Th85;
congr o,b,c, sum b,c,o by Def5;
then A2: congr b,o, sum b,c,o,c by Th89;
congr o, sum a,b,o,c, sum (sum a,b,o),c,o by Def5;
then congr b, sum a,b,o, sum b,c,o, sum (sum a,b,o),c,o by A2, Th90;
hence sum (sum a,b,o),c,o = sum a,(sum b,c,o),o by A1, Th81; :: thesis: verum