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