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
dom (c (#) (- g)) = dom (- g) by VALUED_1:def 5
.= dom g by VALUED_1:8 ;
hence dom (c (#) (- g)) = dom ((- c) (#) g) by VALUED_1:def 5; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (c (#) (- g)) or (c (#) (- g)) . b₁ = ((- c) (#) g) . b₁ )
let x be set ; :: thesis: ( not x in dom (c (#) (- g)) or (c (#) (- g)) . x = ((- c) (#) g) . x )
assume x in dom (c (#) (- g)) ; :: thesis: (c (#) (- g)) . x = ((- c) (#) g) . x
thus (c (#) (- g)) . x = c * ((- g) . x) by VALUED_1:6
.= c * (- (g . x)) by VALUED_1:8
.= (- c) * (g . x)
.= ((- c) (#) g) . x by VALUED_1:6 ; :: thesis: verum