theorem :: NAGATA_1:25

for T being non empty TopSpace
for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds
for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds
F . n is continuous RealMap of T ) holds
ADD "**" F is continuous RealMap of T