let N be non empty ConjNormAlgStr ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: <%a,b%> is right_add-cancelable
let y, z be Element of (Cayley-Dickson N); :: according to ALGSTR_0:def 4 :: thesis: ( not y + <%a,b%> = z + <%a,b%> or y = z )
assume A2: y + <%a,b%> = z + <%a,b%> ; :: thesis: 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; :: thesis: verum