let N be non empty ConjNormAlgStr ; :: thesis: for a, b being Element of N st <%a,b%> is right_complementable holds
( a is right_complementable & b is right_complementable )
let a, b be Element of N; :: thesis: ( <%a,b%> is right_complementable implies ( a is right_complementable & b is right_complementable ) )
set C = Cayley-Dickson N;
given x being Element of (Cayley-Dickson N) such that A1: <%a,b%> + x = 0. (Cayley-Dickson N) ; :: according to ALGSTR_0:def 11 :: thesis: ( a is right_complementable & b is right_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: <%a,b%> + <%x1,x2%> = <%(a + x1),(b + x2)%> by Def9;

hereby :: according to ALGSTR_0:def 11 :: thesis: b is right_complementable

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

end;

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