let g, h be complex-valued Function; :: thesis: - (g + h) = (- g) - h
A1: dom (- (g + h)) = dom (g + h) by VALUED_1:8;
( dom (g + h) = (dom g) /\ (dom h) & dom ((- g) - h) = (dom (- g)) /\ (dom h) ) by VALUED_1:12, VALUED_1:def 1;
hence A2: dom (- (g + h)) = dom ((- g) - h) by A1, VALUED_1:8; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (- (g + h)) or (- (g + h)) . b₁ = ((- g) - h) . b₁ )
let x be object ; :: thesis: ( not x in dom (- (g + h)) or (- (g + h)) . x = ((- g) - h) . x )
assume A3: 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 A1, A3, VALUED_1:def 1
.= (- (g . x)) - (h . x)
.= ((- g) . x) - (h . x) by VALUED_1:8
.= ((- g) - h) . x by A2, A3, VALUED_1:13 ; :: thesis: verum