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