:: deftheorem Def7 defines + NAGATA_1:def 7 :
for T being non empty TopSpace
for F, G, b₄ being RealMap of T holds
( b₄ = F + G iff for t being Element of T holds b₄ . t = (F . t) + (G . t) );