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 <#> g;
A1: dom (<-> (f <#> g)) = dom (f <#> g) by Def33;
( dom (f <#> g) = (dom f) /\ (dom g) & 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
hence (f <#> (- g)) . x = (f . x) (#) ((- g) . x) by Def43
.= (f . x) (#) (- (g . x)) by VALUED_1:8
.= - ((f . x) (#) (g . x)) by Th24
.= - ((f <#> g) . x) by A1, A2, A3, Def43
.= (<-> (f <#> g)) . x by A2, A3, Def33 ;
:: thesis: verum