let a be Real; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (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)) ; :: thesis: verum