let c be complex number ; :: thesis: for g being complex-valued Function holds g (/) (- c) = - (g (/) c)
let g be complex-valued Function; :: thesis: g (/) (- c) = - (g (/) c)
thus g (/) (- c) = (- (1 / c)) (#) g by XCMPLX_1:189
.= - (g (/) c) by Th24 ; :: thesis: verum