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