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:121;

now

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 Function of NAT ,(Funcs the carrier of T,REAL ) such that
A8: f . 1 = F . 1 and
A9: for n being Element of 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:2;
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 13;
A15: n + 0 < n + 1 by XREAL_1:10;
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:10;
then n + 1 in Seg (len F) by A14, FINSEQ_1:3;
then n + 1 in dom F by FINSEQ_1:def 3;
then F . (n + 1) in rng F by FUNCT_1:def 5;
then reconsider fn = f . n, Fn1 = F . (n + 1) as RealMap of T by FUNCT_2:121;
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