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_{1} being object holds

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

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

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

( not 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