let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V holds - f = (- 1r) (#) f
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V holds - f = (- 1r) (#) f
let f be PartFunc of M,V; :: thesis: - f = (- 1r) (#) f
A1: dom (- f) = dom f by VFUNCT_1:def 5
.= dom ((- 1r) (#) f) by Def2 ;
now :: thesis: for c being Element of M st c in dom ((- 1r) (#) f) holds
(- f) /. c = ((- 1r) (#) f) /. c
let c be Element of M; :: thesis: ( c in dom ((- 1r) (#) f) implies (- f) /. c = ((- 1r) (#) f) /. c )
assume A2: c in dom ((- 1r) (#) f) ; :: thesis: (- f) /. c = ((- 1r) (#) f) /. c
hence (- f) /. c = - (f /. c) by A1, VFUNCT_1:def 5
.= (- 1r) * (f /. c) by CLVECT_1:3
.= ((- 1r) (#) f) /. c by A2, Def2 ;
:: thesis: verum
end;
hence - f = (- 1r) (#) f by A1, PARTFUN2:1; :: thesis: verum