let N be non empty ConjNormAlgStr ; for a, b being Element of N st <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable holds
- <%a,b%> = <%(- a),(- b)%>
let a, b be Element of N; ( <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable implies - <%a,b%> = <%(- a),(- b)%> )
assume A1:
( <%a,b%> is left_complementable & <%a,b%> is right_add-cancelable )
; - <%a,b%> = <%(- a),(- b)%>
then
( a is left_complementable & b is left_complementable & a is right_add-cancelable & b is right_add-cancelable )
by Th15, Th23;
then A2:
( (- a) + a = 0. N & (- b) + b = 0. N )
by ALGSTR_0:def 13;
<%(- a),(- b)%> + <%a,b%> =
<%((- a) + a),((- b) + b)%>
by Def9
.=
0. (Cayley-Dickson N)
by A2, Def9
;
hence
- <%a,b%> = <%(- a),(- b)%>
by A1, ALGSTR_0:def 13; verum