let b1, b2 be Element of ; :: 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 Th87;
congr o,a,b1,o by A2, Def5;
then congr a,o,o,b1 by Th87;
hence b1 = b2 by A4, Th81; :: thesis: verum