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