theorem Th31: :: CAYLDICK:31

<%<%(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))%>%>