thus <%<%(0. 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),(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)%> *') * <%(0. N_Real),(0. N_Real)%>))%> by Lm2
.= <%<%(0. N_Real),(1. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%> * <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> by Def9 ; :: thesis: verum