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