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