let F be sequence of ExtREAL; :: thesis: ( ( for n being Element of NAT holds F . n in REAL ) implies for n being Nat holds (Ser F) . n in REAL )

defpred S_{1}[ Nat] means (Ser F) . $1 in REAL ;

assume A1: for n being Element of NAT holds F . n in REAL ; :: thesis: for n being Nat holds (Ser F) . n in REAL

A2: for s being Nat st S_{1}[s] holds

S_{1}[s + 1]

then A4: S_{1}[ 0 ]
by A1;

thus for s being Nat holds S_{1}[s]
from NAT_1:sch 2(A4, A2); :: thesis: verum

defpred S

assume A1: for n being Element of NAT holds F . n in REAL ; :: thesis: for n being Nat holds (Ser F) . n in REAL

A2: for s being Nat st S

S

proof

(Ser F) . 0 = F . 0
by Def11;
let s be Nat; :: thesis: ( S_{1}[s] implies S_{1}[s + 1] )

reconsider b = F . (s + 1) as Element of REAL by A1;

reconsider y = (Ser F) . s as R_eal ;

assume (Ser F) . s in REAL ; :: thesis: S_{1}[s + 1]

then reconsider a = y as Element of REAL ;

A3: y + (F . (s + 1)) = a + b by XXREAL_3:def 2;

(Ser F) . (s + 1) = y + (F . (s + 1)) by Def11;

hence S_{1}[s + 1]
by A3; :: thesis: verum

end;reconsider b = F . (s + 1) as Element of REAL by A1;

reconsider y = (Ser F) . s as R_eal ;

assume (Ser F) . s in REAL ; :: thesis: S

then reconsider a = y as Element of REAL ;

A3: y + (F . (s + 1)) = a + b by XXREAL_3:def 2;

(Ser F) . (s + 1) = y + (F . (s + 1)) by Def11;

hence S

then A4: S

thus for s being Nat holds S