let a be Element of F_Real; :: thesis: 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))
let M be Matrix of 3,F_Real; :: thesis: ( M = symmetric_3 (a,a,(- a),0,0,0) implies (M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0)) )
assume A1: M = symmetric_3 (a,a,(- a),0,0,0) ; :: thesis: (M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0))
reconsider ra2 = a * a as Element of F_Real ;
(M * M) * M = (ra2 * (1. (F_Real,3))) * M by A1, Th40
.= ra2 * ((1. (F_Real,3)) * M) by Th47
.= ra2 * M by MATRIX_3:18
.= ra2 * (a * (symmetric_3 (1,1,(- 1),0,0,0))) by A1, Th48
.= ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0)) by MATRIX_5:11 ;
hence (M * M) * M = ((a * a) * a) * (symmetric_3 (1,1,(- 1),0,0,0)) ; :: thesis: verum