theorem
:: INTEGR15:21
for
n
being
Nat
for
Z
,
x
being
set
for
f
,
g
being
PartFunc
of
Z
,
(
REAL
n
)
st
x
in
dom
(
f
+
g
)
holds
(
f
+
g
)
/.
x
=
(
f
/.
x
)
+
(
g
/.
x
)