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 ;
dom ((<-> f) <#> g) = (dom (<-> f)) /\ (dom g) by Def43;
hence A2: dom (f <#> (- g)) = dom ((<-> f) <#> g) by ; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (f <#> (- g)) or (f <#> (- g)) . b1 = ((<-> f) <#> g) . b1 )

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 ;
thus (f <#> (- g)) . x = (f . x) (#) ((- g) . x) by
.= (f . x) (#) (- (g . x)) by VALUED_1:8
.= (- (f . x)) (#) (g . x) by Th22
.= ((<-> f) . x) (#) (g . x) by
.= ((<-> f) <#> g) . x by ; :: thesis: verum