let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st N is add-associative & N is right_zeroed & N is right_complementable holds
- <%a,b%> = <%(- a),(- b)%>
let a, b be Element of N; :: thesis: ( N is add-associative & N is right_zeroed & N is right_complementable implies - <%a,b%> = <%(- a),(- b)%> )
assume A1: ( N is add-associative & N is right_zeroed & N is right_complementable ) ; :: thesis: - <%a,b%> = <%(- a),(- b)%>
then A2: ( a + (- a) = 0. N & b + (- b) = 0. N ) by RLVECT_1:def 10;
<%a,b%> + <%(- a),(- b)%> = <%(a + (- a)),(b + (- b))%> by Def9
.= 0. (Cayley-Dickson N) by A2, Def9 ;
hence - <%a,b%> = <%(- a),(- b)%> by A1, RLVECT_1:def 10; :: thesis: verum