let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V holds - (- f) = f
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V holds - (- f) = f
let f be PartFunc of C,V; :: thesis: - (- f) = f
thus - (- f) = (- 1) (#) (- f) by Th23
.= (- 1) (#) ((- 1) (#) f) by Th23
.= ((- 1) * (- 1)) (#) f by Th14
.= f by Th18 ; :: thesis: verum