let g, h be complex-valued Function; :: thesis: - (g /" h) = g /" (- h)
A1: dom (- h) = dom h by VALUED_1:8;
( dom (g /" h) = (dom g) /\ (dom h) & dom (g /" (- h)) = (dom g) /\ (dom (- h)) ) by VALUED_1:16;
hence 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 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 VALUED_1:17
.= (g . x) / (- (h . x)) by XCMPLX_1:188
.= (g . x) / ((- h) . x) by VALUED_1:8
.= (g /" (- h)) . x by VALUED_1:17 ; :: thesis: verum