let SAS be Semi_Affine_Space; :: thesis: for a, x, o, y being Element of SAS st sum (a,x,o) = sum (a,y,o) holds
x = y
let a, x, o, y be Element of SAS; :: thesis: ( sum (a,x,o) = sum (a,y,o) implies x = y )
assume A1: sum (a,x,o) = sum (a,y,o) ; :: thesis: x = y
congr o,a,x, sum (a,x,o) by Def5;
then A2: congr a,o, sum (a,x,o),x by Th89;
congr o,a,y, sum (a,y,o) by Def5;
then congr a,o, sum (a,x,o),y by A1, Th89;
hence x = y by A2, Th81; :: thesis: verum