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