let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st <%a,b%> is left_complementable holds
( a is left_complementable & b is left_complementable )
let a, b be Element of N; :: thesis: ( <%a,b%> is left_complementable implies ( a is left_complementable & b is left_complementable ) )
set C = Cayley-Dickson N;
given x being Element of (Cayley-Dickson N) such that A1: x + <%a,b%> = 0. (Cayley-Dickson N) ; :: according to ALGSTR_0:def 10 :: thesis: ( a is left_complementable & b is left_complementable )
consider x1, x2 being Element of N such that
A2: x = <%x1,x2%> by Th12;
A3: 0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
A4: <%x1,x2%> + <%a,b%> = <%(x1 + a),(x2 + b)%> by Def9;

hereby :: according to ALGSTR_0:def 10 :: thesis: b is left_complementable

take x1 = x1; :: thesis: x1 + a = 0. N
thus x1 + a = 0. N by A1, A2, A3, A4, Th3; :: thesis: verum

end;

take x2 ; :: according to ALGSTR_0:def 10 :: thesis: x2 + b = 0. N
thus x2 + b = 0. N by A1, A2, A3, A4, Th3; :: thesis: verum