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
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;
set Fu = Funcs the carrier of T,REAL ;

now

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

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

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

end;

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

A5: len F >= 1

proof

assume len F < 1 ; :: thesis: contradiction
then len F < 1 + 0 ;
then ( len F <= 0 & len F >= 0 ) by NAT_1:13;
hence contradiction by A4; :: thesis: verum

end;

then consider f being Function of NAT ,(Funcs the carrier of T,REAL ) such that
A6: ( f . 1 = F . 1 & ( for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = ADD . (f . n),(F . (n + 1)) ) & ADD "**" F = f . (len F) ) by FINSOP_1:2;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 is continuous RealMap of T );
A7: S₁[1] by A2, A6;
A8: 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 A9: ( n >= 1 & S₁[n] ) ; :: thesis: S₁[n + 1]
assume A10: n + 1 <= len F ; :: thesis: f . (n + 1) is continuous RealMap of T
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 0 < n + 1 by XREAL_1:10;
then A11: ( n <= len F & n < len F & n <> 0 & n + 1 <> 0 ) by A9, A10, XXREAL_0:2;
1 + 0 <= n + 1 by A9, XREAL_1:10;
then n + 1 in Seg (len F) by A10, 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 & fn is continuous & f . (n + 1) = ADD . (f . n),(F . (n + 1)) ) by A2, A6, A9, A10, A11;
then ( fn + Fn1 is continuous & f . (n + 1) = fn + Fn1 ) by A1, Th22;
hence f . (n + 1) is continuous RealMap of T ; :: thesis: verum

end;

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

end;

end;

end;

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