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