theorem Th34: :: CAYLDICK:34

(<%<%<%(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),(0. N_Real)%>,<%(0. N_Real),(0. N_Real)%>%>,<%<%(0. N_Real),(0. N_Real)%>,<%(- (1. N_Real)),(0. N_Real)%>%>%>