let f be complex-valued Function; :: thesis: ( dom (- f) = dom f & ( for c being object holds (- f) . c = - (f . c) ) )
thus A1: dom (- f) = dom f by Def5; :: thesis: for c being object holds (- f) . c = - (f . c)
let c be object ; :: thesis: (- f) . c = - (f . c)

per cases ( c in dom f or not c in dom f ) ;

suppose c in dom f ; :: thesis: (- f) . c = - (f . c)

hence (- f) . c = (- 1) * (f . c) by A1, Def5
.= - (f . c) ;
:: thesis: verum

end;

suppose A2: not c in dom f ; :: thesis: (- f) . c = - (f . c)

hence (- f) . c = - 0 by A1, FUNCT_1:def 2
.= - (f . c) by A2, FUNCT_1:def 2 ;
:: thesis: verum

end;

end;