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
;
verum