let V be RealLinearSpace; :: thesis: for L being linear-Functional of V
for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
let L be linear-Functional of V; :: thesis: for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)
let v1, v2 be VECTOR of V; :: thesis: L . (v1 - v2) = (L . v1) - (L . v2)
thus L . (v1 - v2) = (L . v1) + (L . (- v2)) by Def2
.= (L . v1) + (- (L . v2)) by Th18
.= (L . v1) - (L . v2) ; :: thesis: verum