let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds Sum <*v,v*> = 2 * v
let v be VECTOR of V; :: thesis: Sum <*v,v*> = 2 * v
thus Sum <*v,v*> = v + v by Th45
.= (1 * v) + v by Def8
.= (1 * v) + (1 * v) by Def8
.= (1 + 1) * v by Def6
.= 2 * v ; :: thesis: verum