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