theorem Th30: :: CAYLDICK:30

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