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