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
thus Sum <*v,v*> = v + v by RLVECT_1:62
.= (1r * v) + v by Def2
.= (1r * v) + (1r * v) by Def2
.= (1r + 1r ) * v by Def2 ; :: thesis: verum