let c be complex number ; :: thesis: for g being complex-valued Function holds (- c) (#) g = - (c (#) g)
let g be complex-valued Function; :: thesis: (- c) (#) g = - (c (#) g)
thus (- c) (#) g = c (#) (- g) by Th22
.= - (c (#) g) by Th23 ; :: thesis: verum