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 b1 being Element of (Cayley-Dickson N) st b1 = <%a,b%> holds
not b1 is zero ; :: thesis: verum