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:84
.= ((1r + 1r ) * v) + v by Th18
.= ((1r + 1r ) * v) + (1r * v) by Def2
.= ((1r + 1r ) + 1r ) * v by Def2
.= (2r + 1r ) * v
.= ((1r + 1r ) + 1r ) * v ; :: thesis: verum