let X, X1, X2 be set ; :: thesis: for Y, Y1, Y2 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)
let Y, Y1, Y2 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2
for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)
let f1 be PartFunc of X1,Y1; :: thesis: for f2 being PartFunc of X2,Y2
for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)
let f2 be PartFunc of X2,Y2; :: thesis: for g being complex-valued Function st f1 = f <+> g & f2 = <-> f holds
<-> f1 = f2 <+> (- g)
let g be complex-valued Function; :: thesis: ( f1 = f <+> g & f2 = <-> f implies <-> f1 = f2 <+> (- g) )
assume that
A1: f1 = f <+> g and
A2: f2 = <-> f ; :: thesis: <-> f1 = f2 <+> (- g)
A3: dom (<-> f1) = dom f1 by Def32;
A4: dom f1 = (dom f) /\ (dom g) by A1, Def40;
A5: dom f2 = dom f by A2, Def32;
dom (- g) = dom g by VALUED_1:8;
hence A7: dom (<-> f1) = dom (f2 <+> (- g)) by A3, A4, A5, Def40; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (<-> f1) or (<-> f1) . b₁ = (f2 <+> (- g)) . b₁ )
let x be set ; :: thesis: ( not x in dom (<-> f1) or (<-> f1) . x = (f2 <+> (- g)) . x )
assume A8: x in dom (<-> f1) ; :: thesis: (<-> f1) . x = (f2 <+> (- g)) . x
then A9: x in dom f2 by A3, A4, A5, XBOOLE_0:def 4;
thus (<-> f1) . x = - (f1 . x) by A8, Def32
.= - ((f . x) + (g . x)) by A1, A3, A8, Def40
.= (- (f . x)) - (g . x) by Th81
.= (- (f . x)) + ((- g) . x) by VALUED_1:8
.= (f2 . x) + ((- g) . x) by A2, A9, Def32
.= (f2 <+> (- g)) . x by A7, A8, Def40 ; :: thesis: verum