let K be non empty addLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let V be non empty ModuleStr over K; :: thesis: for f, g being Functional of V
for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let f, g be Functional of V; :: thesis: for v being Vector of V holds (f - g) . v = (f . v) - (g . v)
let v be Vector of V; :: thesis: (f - g) . v = (f . v) - (g . v)
thus (f - g) . v = (f . v) + ((- g) . v) by HAHNBAN1:def 3
.= (f . v) - (g . v) by HAHNBAN1:def 4 ; :: thesis: verum