let N be non empty ConjNormAlgStr ; for a, b being Element of N st <%a,b%> is left_add-cancelable holds
( a is left_add-cancelable & b is left_add-cancelable )
let a, b be Element of N; ( <%a,b%> is left_add-cancelable implies ( a is left_add-cancelable & b is left_add-cancelable ) )
assume A1:
<%a,b%> is left_add-cancelable
; ( a is left_add-cancelable & b is left_add-cancelable )
let y, z be Element of N; ALGSTR_0:def 3 ( not b + y = b + z or y = z )
assume A3:
b + y = b + z
; y = z
<%a,b%> + <%(0. N),y%> =
<%(a + (0. N)),(b + y)%>
by Def9
.=
<%a,b%> + <%(0. N),z%>
by A3, Def9
;
then
<%(0. N),y%> = <%(0. N),z%>
by A1;
hence
y = z
by Th3; verum