for a being Element of F_Real
for M being Matrix of 3,F_Real st M = symmetric_3 (a,a,(- a),0,0,0) holds
(M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0))