let X be set ; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y
for g being complex-valued Function holds f <#> (- g) = (<-> f) <#> g
let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for g being complex-valued Function holds f <#> (- g) = (<-> f) <#> g
let f be PartFunc of X,Y; :: thesis: for g being complex-valued Function holds f <#> (- g) = (<-> f) <#> g
let g be complex-valued Function; :: thesis: f <#> (- g) = (<-> f) <#> g
set f1 = <-> f;
A1: ( dom (<-> f) = dom f & dom (f <#> (- g)) = (dom f) /\ (dom (- g)) ) by Def33, Def43;
dom ((<-> f) <#> g) = (dom (<-> f)) /\ (dom g) by Def43;
hence A2: dom (f <#> (- g)) = dom ((<-> f) <#> g) by A1, VALUED_1:8; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (f <#> (- g)) or (f <#> (- g)) . b₁ = ((<-> f) <#> g) . b₁ )
let x be object ; :: thesis: ( not x in dom (f <#> (- g)) or (f <#> (- g)) . x = ((<-> f) <#> g) . x )
assume A3: x in dom (f <#> (- g)) ; :: thesis: (f <#> (- g)) . x = ((<-> f) <#> g) . x
then A4: x in dom (<-> f) by A1, XBOOLE_0:def 4;
thus (f <#> (- g)) . x = (f . x) (#) ((- g) . x) by A3, Def43
.= (f . x) (#) (- (g . x)) by VALUED_1:8
.= (- (f . x)) (#) (g . x) by Th22
.= ((<-> f) . x) (#) (g . x) by A4, Def33
.= ((<-> f) <#> g) . x by A2, A3, Def43 ; :: thesis: verum