set C = Cayley-Dickson N;

now :: thesis: not <%a,b%> is zero

assume <%a,b%> is zero ; :: thesis: contradiction
then A1: <%a,b%> = 0. (Cayley-Dickson N) ;
0. (Cayley-Dickson N) = <%(0. N),(0. N)%> by Def9;
hence contradiction by A1, Th3; :: thesis: verum

end;

hence for b₁ being Element of (Cayley-Dickson N) st b₁ = <%a,b%> holds
not b₁ is zero ; :: thesis: verum