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