let V be ComplexLinearSpace; :: thesis: for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v
let v be VECTOR of V; :: thesis: Sum <*(- v),(- v)*> = (- (1r + 1r)) * v
reconsider 2r = 2 + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum <*(- v),(- v)*> = - (v + v) by RLVECT_1:60
.= - (Sum <*v,v*>) by RLVECT_1:45
.= - ((1r + 1r) * v) by Th17
.= (- 1r) * (2r * v) by Th3
.= ((- 1r) * 2r) * v by Def4
.= (- (1r + 1r)) * v ; :: thesis: verum