let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,the carrier of V holds - (- f) = f
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,the carrier of V holds - (- f) = f
let f be PartFunc of M,the carrier of 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 7 ; :: thesis: verum