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
A1: dom (- (g + c)) = dom (g + c) by VALUED_1:8;
A2: ( dom (g + c) = dom g & dom ((- g) - c) = dom (- g) ) by VALUED_1:def 2;
hence dom (- (g + c)) = dom ((- g) - c) by A1, VALUED_1:8; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (- (g + c)) or (- (g + c)) . b₁ = ((- g) - c) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (- (g + c)) or (- (g + c)) . x = ((- g) - c) . x )
assume A3: x in dom (- (g + c)) ; :: thesis: (- (g + c)) . x = ((- g) - c) . x
A4: dom (- g) = dom g by VALUED_1:8;
thus (- (g + c)) . x = - ((g + c) . x) by VALUED_1:8
.= - ((g . x) + c) by A1, A3, VALUED_1:def 2
.= (- (g . x)) - c
.= ((- g) . x) - c by VALUED_1:8
.= ((- g) - c) . x by A2, A1, A4, A3, VALUED_1:def 2 ; :: thesis: verum