let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st a is right_complementable & b is right_complementable holds
<%a,b%> is right_complementable
let a, b be Element of N; :: thesis: ( a is right_complementable & b is right_complementable implies <%a,b%> is right_complementable )
given x being Element of N such that A1: a + x = 0. N ; :: according to ALGSTR_0:def 11 :: thesis: ( not b is right_complementable or <%a,b%> is right_complementable )
given y being Element of N such that A2: b + y = 0. N ; :: according to ALGSTR_0:def 11 :: thesis: <%a,b%> is right_complementable
take <%x,y%> ; :: according to ALGSTR_0:def 11 :: thesis: <%a,b%> + <%x,y%> = 0. (Cayley-Dickson N)
thus <%a,b%> + <%x,y%> = <%(a + x),(b + y)%> by Def9
.= 0. (Cayley-Dickson N) by A1, A2, Def9 ; :: thesis: verum