let N1, N2 be Matrix of 3,F_Real; :: thesis: ( 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))*>*> implies N1 is_reverse_of N2 )
assume A1: ( 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))*>*> ) ; :: thesis: N1 is_reverse_of N2
( N2 * N1 = 1. (F_Real,3) & N1 * N2 = 1. (F_Real,3) ) by A1, Th11, Th12, ANPROJ_9:1;
hence N1 is_reverse_of N2 by MATRIX_6:def 2; :: thesis: verum