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:45
.= (1r * v) + v by Def5
.= (1r * v) + (1r * v) by Def5
.= (1r + 1r) * v by Def3 ; :: thesis: verum