theorem Th32: :: CAYLDICK:32

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