let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st a is left_add-cancelable & b is left_add-cancelable holds
<%a,b%> is left_add-cancelable
let a, b be Element of N; :: thesis: ( a is left_add-cancelable & b is left_add-cancelable implies <%a,b%> is left_add-cancelable )
assume A1: ( a is left_add-cancelable & b is left_add-cancelable ) ; :: thesis: <%a,b%> is left_add-cancelable
let y, z be Element of (Cayley-Dickson N); :: according to ALGSTR_0:def 3 :: thesis: ( not <%a,b%> + y = <%a,b%> + z or y = z )
assume A2: <%a,b%> + y = <%a,b%> + z ; :: 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;
( <%a,b%> + <%y1,y2%> = <%(a + y1),(b + y2)%> & <%a,b%> + <%z1,z2%> = <%(a + z1),(b + z2)%> ) by Def9;
then ( a + y1 = a + z1 & b + y2 = b + z2 ) by A2, A3, A4, Th3;
then ( y1 = z1 & y2 = z2 ) by A1;
hence y = z by A3, A4; :: thesis: verum