let N be non empty ConjNormAlgStr ; for a, b being Element of N st a is right_add-cancelable & b is right_add-cancelable holds
<%a,b%> is right_add-cancelable
let a, b be Element of N; ( a is right_add-cancelable & b is right_add-cancelable implies <%a,b%> is right_add-cancelable )
assume A1:
( a is right_add-cancelable & b is right_add-cancelable )
; <%a,b%> is right_add-cancelable
let y, z be Element of (Cayley-Dickson N); ALGSTR_0:def 4 ( not y + <%a,b%> = z + <%a,b%> or y = z )
assume A2:
y + <%a,b%> = z + <%a,b%>
; y = z
consider y1, y2 being Element of N such that
A3:
y = <%y1,y2%>
by Th12;
consider z1, z2 being Element of N such that
A4:
z = <%z1,z2%>
by Th12;
( <%y1,y2%> + <%a,b%> = <%(y1 + a),(y2 + b)%> & <%z1,z2%> + <%a,b%> = <%(z1 + a),(z2 + b)%> )
by Def9;
then
( y1 + a = z1 + a & y2 + b = z2 + b )
by A2, A3, A4, Th3;
then
( y1 = z1 & y2 = z2 )
by A1;
hence
y = z
by A3, A4; verum