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