let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds - (- f) = f
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V holds - (- f) = f
let f be PartFunc of M,V; :: thesis: - (- f) = f
thus - (- f) = (- 1r) (#) (- f) by Th23
.= (- 1r) (#) ((- 1r) (#) f) by Th23
.= ((- 1r) * (- 1r)) (#) f by Th14
.= f by Th18, COMPLEX1:def 4 ; :: thesis: verum