let N be non empty ConjNormAlgStr ; :: thesis: 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; :: thesis: ( <%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 ; :: thesis: ( a is right_add-cancelable & b is right_add-cancelable )

hereby :: according to ALGSTR_0:def 4 :: thesis: b is right_add-cancelable

let y, z be Element of N; :: thesis: ( y + a = z + a implies y = z )
assume A2: y + a = z + a ; :: thesis: y = z
<%y,(0. N)%> + <%a,b%> = <%(y + a),((0. N) + b)%> by Def9
.= <%z,(0. N)%> + <%a,b%> by A2, Def9 ;
then <%y,(0. N)%> = <%z,(0. N)%> by A1;
hence y = z by Th3; :: thesis: verum

end;

let y, z be Element of N; :: according to ALGSTR_0:def 4 :: thesis: ( not y + b = z + b or y = z )
assume A3: y + b = z + b ; :: thesis: 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; :: thesis: verum