let g, h be complex-valued Function; :: thesis: - (g + h) = (- g) - h
A1: dom (g + h) = (dom g) /\ (dom h) by VALUED_1:def 1;
a1: dom ((- g) - h) = (dom (- g)) /\ (dom h) by VALUED_1:12;
A2: dom (- (g + h)) = dom (g + h) by VALUED_1:8;
hence A3: dom (- (g + h)) = dom ((- g) - h) by A1, a1, VALUED_1:8; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (- (g + h)) or (- (g + h)) . b₁ = ((- g) - h) . b₁ )
let x be set ; :: thesis: ( not x in dom (- (g + h)) or (- (g + h)) . x = ((- g) - h) . x )
assume A4: x in dom (- (g + h)) ; :: thesis: (- (g + h)) . x = ((- g) - h) . x
thus (- (g + h)) . x = - ((g + h) . x) by VALUED_1:8
.= - ((g . x) + (h . x)) by A2, A4, VALUED_1:def 1
.= (- (g . x)) - (h . x)
.= ((- g) . x) - (h . x) by VALUED_1:8
.= ((- g) - h) . x by A3, A4, VALUED_1:13 ; :: thesis: verum