let T be non empty TopSpace; :: thesis: 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
let ADD be BinOp of (Funcs ( the carrier of T,REAL)); :: thesis: ( ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) implies 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 )
assume A1: for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ; :: thesis: 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
set Fu = Funcs ( the carrier of T,REAL);
let F be FinSequence of Funcs ( the carrier of T,REAL); :: thesis: ( ( for n being Element of NAT st 0 <> n & n <= len F holds
F . n is continuous RealMap of T ) implies ADD "**" F is continuous RealMap of T )
assume A2: for n being Element of NAT st 0 <> n & n <= len F holds
F . n is continuous RealMap of T ; :: thesis: ADD "**" F is continuous RealMap of T
reconsider ADDF = ADD "**" F as RealMap of T by FUNCT_2:66;

now :: thesis: ADD "**" F is continuous RealMap of T

per cases ( len F = 0 or len F <> 0 ) ;

suppose A3: len F = 0 ; :: thesis: ADD "**" F is continuous RealMap of T

A4: ADD is having_a_unity by A1, Th23;
then ex x being Element of Funcs ( the carrier of T,REAL) st x is_a_unity_wrt ADD by SETWISEO:def 2;
then A5: the_unity_wrt ADD is_a_unity_wrt ADD by BINOP_1:def 8;
ADDF = the_unity_wrt ADD by A3, A4, FINSOP_1:def 1;
hence ADD "**" F is continuous RealMap of T by A1, A5, Th24; :: thesis: verum

end;

suppose A6: len F <> 0 ; :: thesis: ADD "**" F is continuous RealMap of T

A7: len F >= 1

proof

assume len F < 1 ; :: thesis: contradiction
then len F < 1 + 0 ;
hence contradiction by A6, NAT_1:13; :: thesis: verum

end;

then consider f being sequence of (Funcs ( the carrier of T,REAL)) such that
A8: f . 1 = F . 1 and
A9: for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = ADD . ((f . n),(F . (n + 1))) and
A10: ADD "**" F = f . (len F) by FINSOP_1:1;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 is continuous RealMap of T );
A11: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume that
A12: n >= 1 and
A13: S₁[n] ; :: thesis: S₁[n + 1]
assume A14: n + 1 <= len F ; :: thesis: f . (n + 1) is continuous RealMap of T
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A15: n + 0 < n + 1 by XREAL_1:8;
then n < len F by A14, XXREAL_0:2;
then A16: f . (n + 1) = ADD . ((f . n),(F . (n + 1))) by A9, A12;
1 + 0 <= n + 1 by A12, XREAL_1:8;
then n + 1 in Seg (len F) by A14, FINSEQ_1:1;
then n + 1 in dom F by FINSEQ_1:def 3;
then F . (n + 1) in rng F by FUNCT_1:def 3;
then reconsider fn = f . n, Fn1 = F . (n + 1) as RealMap of T by FUNCT_2:66;
Fn1 is continuous by A2, A14;
then fn + Fn1 is continuous by A13, A14, A15, Th22, XXREAL_0:2;
hence f . (n + 1) is continuous RealMap of T by A1, A16; :: thesis: verum

end;

A17: S₁[1] by A2, A8;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A17, A11);
hence ADD "**" F is continuous RealMap of T by A7, A10; :: thesis: verum

end;

end;

end;

hence ADD "**" F is continuous RealMap of T ; :: thesis: verum