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;
set f2 = <-> f;
A1: dom (<-> (f <+> g)) = dom (f <+> g) by Def33;
A2: ( dom (f <+> g) = (dom f) /\ (dom g) & dom (<-> f) = dom f ) by ;
dom (- g) = dom g by VALUED_1:8;
hence A3: 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 A4: x in dom (<-> (f <+> g)) ; :: thesis: (<-> (f <+> g)) . x = ((<-> f) <+> (- g)) . x
then A5: x in dom (<-> f) by ;
thus (<-> (f <+> g)) . x = - ((f <+> g) . x) by
.= - ((f . x) + (g . x)) by
.= (- (f . x)) - (g . x) by Th10
.= (- (f . x)) + ((- g) . x) by VALUED_1:8
.= ((<-> f) . x) + ((- g) . x) by
.= ((<-> f) <+> (- g)) . x by ; :: thesis: verum