set a1 = (<%<%(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)%>,<%(0. N_Real),(0. N_Real)%>%> *') * <%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>);
set b1 = (<%<%(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)%>%> *'));
A1: <%(0. N_Real),(1. N_Real)%> * (<%(0. N_Real),(1. N_Real)%> *') = <%(((0. N_Real) * (0. N_Real)) - (((- (1. N_Real)) *') * (1. N_Real))),(((- (1. N_Real)) * (0. N_Real)) + ((1. N_Real) * ((0. N_Real) *')))%> by Lm3, Def9;
A2: <%(1. N_Real),(0. N_Real)%> * <%(0. N_Real),(1. N_Real)%> = <%(((1. N_Real) * (0. N_Real)) - (((1. N_Real) *') * (0. N_Real))),(((1. N_Real) * (1. N_Real)) + ((0. N_Real) * ((0. N_Real) *')))%> by Def9;
(<%<%(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)%>)),((<%(1. N_Real),(0. N_Real)%> * <%(0. N_Real),(1. N_Real)%>) + (<%(0. N_Real),(0. N_Real)%> * (<%(0. N_Real),(0. N_Real)%> *')))%> by Def9
.= <%<%(0. N_Real),(0. N_Real)%>,(<%(1. N_Real),(0. N_Real)%> * <%(0. N_Real),(1. N_Real)%>)%> ;
then A3: ((<%<%(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)%>%> = <%((<%(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)%> * <%(0. N_Real),(0. N_Real)%>) + (<%(0. N_Real),(1. N_Real)%> * (<%(0. N_Real),(1. N_Real)%> *')))%> by A2, Def9
.= <%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%> by A1 ;
<%<%<%(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)%>%>%> = <%((<%<%(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)%>,<%(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)%>,<%(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)%>%> *')))%> by Def9;
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),(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)%>%> * ((<%<%(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)%>,<%(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)%>,<%(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),(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)%>,<%(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)%>%>) + (<%<%(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),(1. N_Real)%>,<%(0. 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),(0. N_Real)%>%>,(((<%<%(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)%>%>)%>
.= <%<%<%(0. N_Real),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(1. N_Real),(0. N_Real)%>%>%> by A3 ;
:: thesis: verum