let SAS be Semi_Affine_Space; :: thesis: for a, o being Element of ex x being Element of st sum a,x,o = o
let a, o be Element of ; :: thesis: ex x being Element of st sum a,x,o = o
consider x being Element of such that
A1: congr a,o,o,x by Th82;
A2: congr o,a,x, sum a,x,o by Def5;
congr o,a,x,o by A1, Th89;
hence ex x being Element of st sum a,x,o = o by A2, Th81; :: thesis: verum