let a be non zero Real; :: thesis: (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = 1. (F_Real,3)
reconsider z1 = 0 , z2 = a, z3 = - a as Element of F_Real by XREAL_0:def 1;
A1: symmetric_3 (a,a,(- a),0,0,0) = <*<*z2,z1,z1*>,<*z1,z2,z1*>,<*z1,z1,z3*>*> by PASCAL:def 3;
A2: ( z2 * (1 / z2) = 1 & z3 * (1 / z3) = 1 ) by XCMPLX_1:106;
reconsider y1 = z1, y2 = 1 / z2, y3 = 1 / z3 as Element of F_Real by XREAL_0:def 1;
A3: symmetric_3 (y2,y2,y3,y1,y1,y1) = <*<*(1 / z2),z1,z1*>,<*z1,(1 / z2),z1*>,<*z1,z1,(1 / z3)*>*> by PASCAL:def 3;
(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = (symmetric_3 (z2,z2,z3,z1,z1,z1)) * (symmetric_3 (y2,y2,y3,y1,y1,y1)) by XCMPLX_1:188
.= <*<*(((z2 * y2) + (z1 * y1)) + (z1 * y1)),(((z2 * y1) + (z1 * y2)) + (z1 * y1)),(((z2 * y1) + (z1 * y1)) + (z1 * y3))*>,<*(((z1 * y2) + (z2 * y1)) + (z1 * y1)),(((z1 * y1) + (z2 * y2)) + (z1 * y1)),(((z1 * y1) + (z2 * y1)) + (z1 * y3))*>,<*(((z1 * y2) + (z1 * y1)) + (z3 * y1)),(((z1 * y1) + (z1 * y2)) + (z3 * y1)),(((z1 * y1) + (z1 * y1)) + (z3 * y3))*>*> by A1, A3, ANPROJ_9:6
.= <*<*1,0,0*>,<*0,1,0*>,<*0,0,1*>*> by A2 ;
hence (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = 1. (F_Real,3) by ANPROJ_9:1; :: thesis: verum