reconsider a = 1 as non zero Real ;
- (1 / a) = - 1 ;
hence (symmetric_3 (1,1,(- 1),0,0,0)) * (symmetric_3 (1,1,(- 1),0,0,0)) = 1. (F_Real,3) by Th41; :: thesis: verum