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: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)
.= ((- g) . x) / (h . x) by VALUED_1:8
.= ((- g) /" h) . x by VALUED_1:17 ; :: thesis: verum