for a being 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))