let a be real number ; :: thesis: for V being RealLinearSpace
for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
let V be RealLinearSpace; :: thesis: for v, w being VECTOR of V holds a * (v - w) = (a * v) - (a * w)
let v, w be VECTOR of V; :: thesis: a * (v - w) = (a * v) - (a * w)
thus a * (v - w) = (a * v) + (a * (- w)) by Def9
.= (a * v) - (a * w) by Th39 ; :: thesis: verum