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, sum a,b,o,c, sum (sum a,b,o),c,o & congr o,a, sum b,c,o, sum a,(sum b,c,o),o & congr o,b,c, sum b,c,o ) by Def5;
then ( congr b, sum a,b,o, sum b,c,o, sum a,(sum b,c,o),o & congr b,o, sum b,c,o,c & congr o, sum a,b,o,c, sum (sum a,b,o),c,o ) by Th85, Th89;
then ( congr b, sum a,b,o, sum b,c,o, sum a,(sum b,c,o),o & congr b, sum a,b,o, sum b,c,o, sum (sum a,b,o),c,o ) by Th90;
hence sum (sum a,b,o),c,o = sum a,(sum b,c,o),o by Th81; :: thesis: verum