let c be Complex; :: 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_{1} being object holds

( not b_{1} in dom (- (g + c)) or (- (g + c)) . b_{1} = ((- g) - c) . b_{1} )

let x be object ; :: thesis: ( not x in dom (- (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

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

( not b

let x be object ; :: thesis: ( not x in dom (- (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