theorem Th48: :: BKMODEL1:56

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