let b1, b2 be Element of SAS; ( 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
; 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; verum