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