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) = - (g (/) c) by Th31
.= (- g) (/) c by Th30 ; :: thesis: verum