let N1, N2 be Matrix of 3,F_Real; :: thesis: ( N2 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> & N1 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> implies N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*> )
assume that
A1: N2 = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> and
A2: N1 = <*<*(2 / 3),0,(- (1 / 3))*>,<*0,(1 / (sqrt 3)),0*>,<*(1 / 3),0,(- (2 / 3))*>*> ; :: thesis: N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*>
reconsider a9 = 2, b9 = 0 , c9 = - 1, d9 = 0 , e9 = sqrt 3, f9 = 0 , g9 = 1, h9 = 0 , i9 = - 2, a = 2 / 3, b = 0 , c = - (1 / 3), d = 0 , e = 1 / (sqrt 3), f = 0 , g = 1 / 3, h = 0 , i = - (2 / 3) as Element of F_Real by XREAL_0:def 1;
reconsider n11 = ((a * a9) + (b * d9)) + (c * g9), n12 = ((a * b9) + (b * e9)) + (c * h9), n13 = ((a * c9) + (b * f9)) + (c * i9), n21 = ((d * a9) + (e * d9)) + (f * g9), n22 = ((d * b9) + (e * e9)) + (f * h9), n23 = ((d * c9) + (e * f9)) + (f * i9), n31 = ((g * a9) + (h * d9)) + (i * g9), n32 = ((g * b9) + (h * e9)) + (i * h9), n33 = ((g * c9) + (h * f9)) + (i * i9) as Element of F_Real ;
( n11 = 1 & n12 = 0 & n13 = 0 & n21 = 0 & n22 = 1 & n23 = 0 & n31 = 0 & n32 = 0 & n33 = 1 ) by SQUARE_1:24, XCMPLX_1:106;
hence N1 * N2 = <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*> by A1, A2, Th10; :: thesis: verum