let a be Real; for ra2 being Element of F_Real st ra2 = a * a holds
(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))
let ra2 be Element of F_Real; ( ra2 = a * a implies (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3)) )
assume A1:
ra2 = a * a
; (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))
reconsider zone = 1, z1 = 0 , z2 = a, z3 = - a as Element of F_Real by XREAL_0:def 1;
symmetric_3 (a,a,(- a),0,0,0) = <*<*z2,z1,z1*>,<*z1,z2,z1*>,<*z1,z1,z3*>*>
by PASCAL:def 3;
then (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) =
<*<*(((z2 * z2) + (z1 * z1)) + (z1 * z1)),(((z2 * z1) + (z1 * z2)) + (z1 * z1)),(((z2 * z1) + (z1 * z1)) + (z1 * z3))*>,<*(((z1 * z2) + (z2 * z1)) + (z1 * z1)),(((z1 * z1) + (z2 * z2)) + (z1 * z1)),(((z1 * z1) + (z2 * z1)) + (z1 * z3))*>,<*(((z1 * z2) + (z1 * z1)) + (z3 * z1)),(((z1 * z1) + (z1 * z2)) + (z3 * z1)),(((z1 * z1) + (z1 * z1)) + (z3 * z3))*>*>
by ANPROJ_9:6
.=
<*<*(ra2 * zone),(ra2 * z1),(ra2 * z1)*>,<*(ra2 * z1),(ra2 * zone),(ra2 * z1)*>,<*(ra2 * z1),(ra2 * z1),(ra2 * zone)*>*>
by A1
.=
ra2 * (1. (F_Real,3))
by Th39, ANPROJ_9:1
;
hence
(symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = ra2 * (1. (F_Real,3))
; verum