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 11 :: 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