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