let a be Element of F_Real; :: thesis: symmetric_3 (a,a,(- a),0,0,0) = a * (symmetric_3 (1,1,(- 1),0,0,0))
reconsider z0 = 0 , z1 = 1, z2 = - 1 as Element of F_Real by XREAL_0:def 1;
symmetric_3 (1,1,(- 1),0,0,0) = <*<*z1,z0,z0*>,<*z0,z1,z0*>,<*z0,z0,z2*>*> by PASCAL:def 3;
then a * (symmetric_3 (1,1,(- 1),0,0,0)) = <*<*(a * z1),(a * z0),(a * z0)*>,<*(a * z0),(a * z1),(a * z0)*>,<*(a * z0),(a * z0),(a * z2)*>*> by Th39;
hence symmetric_3 (a,a,(- a),0,0,0) = a * (symmetric_3 (1,1,(- 1),0,0,0)) by PASCAL:def 3; :: thesis: verum