<%(0. N_Real),(1. N_Real)%> *' = <%((0. N_Real) *'),(- (1. N_Real))%>
by Def9;
then
(<%(0. N_Real),(1. N_Real)%> *') * <%(1. N_Real),(0. N_Real)%> = <%(((0. N_Real) * (1. N_Real)) - (((0. N_Real) *') * (- (1. N_Real)))),(((0. N_Real) * (0. N_Real)) + (((1. N_Real) *') * (- (1. N_Real))))%>
by Def9;
hence <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(- (1. N_Real))%>%> =
<%((<%(0. N_Real),(0. N_Real)%> * <%(0. N_Real),(1. N_Real)%>) - ((<%(0. N_Real),(0. N_Real)%> *') * <%(1. N_Real),(0. N_Real)%>)),((<%(0. N_Real),(0. N_Real)%> * <%(0. N_Real),(0. N_Real)%>) + ((<%(0. N_Real),(1. N_Real)%> *') * <%(1. N_Real),(0. N_Real)%>))%>
.=
<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>
by Def9
;
verum