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