let SAS be Semi_Affine_Space; :: thesis: for a, b, c, o being Element of SAS holds sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o)
let a, b, c, o 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 Th65;
congr o,b,c, sum (b,c,o) by Def5;
then A2: congr b,o, sum (b,c,o),c by Th69;
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, Th70;
hence sum ((sum (a,b,o)),c,o) = sum (a,(sum (b,c,o)),o) by A1, Th62; :: thesis: verum