let SAS be Semi_Affine_Space; :: thesis: for a, o being Element of SAS ex x being Element of SAS st sum (a,x,o) = o
let a, o be Element of SAS; :: thesis: ex x being Element of SAS st sum (a,x,o) = o
consider x being Element of SAS such that
A1: congr a,o,o,x by Th63;
A2: congr o,a,x, sum (a,x,o) by Def5;
congr o,a,x,o by A1, Th69;
hence ex x being Element of SAS st sum (a,x,o) = o by A2, Th62; :: thesis: verum