let b1, b2 be Element of SAS; :: thesis: ( sum (a,b1,o) = o & sum (a,b2,o) = o implies b1 = b2 )
assume that
A2: sum (a,b1,o) = o and
A3: sum (a,b2,o) = o ; :: thesis: b1 = b2
congr o,a,b2,o by A3, Def5;
then A4: congr a,o,o,b2 by Th67;
congr o,a,b1,o by A2, Def5;
then congr a,o,o,b1 by Th67;
hence b1 = b2 by A4, Th62; :: thesis: verum