theorem Th11: :: BKMODEL4:20

for N1, N2 being Matrix of 3,F_Real st N1 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> & N2 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> holds
N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>