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