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> ), m2 = (- 2) + (0 * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum <*(- v),(- v)*> = - (v + v) by RLVECT_1:78
.= - (Sum <*v,v*>) by RLVECT_1:62
.= - ((1r + 1r ) * v) by Th18
.= - (2r * v)
.= (- 1r ) * (2r * v) by Th4
.= ((- 1r ) * 2r) * v by Def4
.= (- (1r + 1r )) * v ; :: thesis: verum