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:def 4;
hence dom (- (g (#) h)) = dom ((- g) (#) h) by A1, VALUED_1:8; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in proj1 (- (g (#) h)) or (- (g (#) h)) . b₁ = ((- g) (#) h) . b₁ )
let x be set ; :: thesis: ( not x in proj1 (- (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:5
.= (- (g . x)) * (h . x)
.= ((- g) . x) * (h . x) by VALUED_1:8
.= ((- g) (#) h) . x by VALUED_1:5 ; :: thesis: verum