::
deftheorem
defines
+
ASYMPT_0:def 18 :
for
X
being non
empty
set
for
F
,
G
being
FUNCTION_DOMAIN
of
X
,
REAL
holds
F
+
G
=
{
t
where
t
is
Element
of
Funcs
(
X
,
REAL
) : ex
f
,
g
being
Element
of
Funcs
(
X
,
REAL
) st
(
f
in
F
&
g
in
G
& ( for
n
being
Element
of
X
holds
t
.
n
=
(
f
.
n
)
+
(
g
.
n
)
) )
}
;