let F be sequence of ExtREAL; :: thesis: for n being Nat st F is nonnegative holds

( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )

let n be Nat; :: thesis: ( F is nonnegative implies ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) )

assume A0: F is nonnegative ; :: thesis: ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )

set FF = Ser F;

defpred S_{1}[ Nat] means ( (Ser F) . $1 <= (Ser F) . ($1 + 1) & 0. <= (Ser F) . $1 );

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

A1: (Ser F) . (0 + 1) = y + (F . 1) by Def11;

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

S_{1}[k + 1]

then A6: S_{1}[ 0 ]
by A1, XXREAL_3:39, A0, Th38;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A2);

hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) ; :: thesis: verum

( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )

let n be Nat; :: thesis: ( F is nonnegative implies ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) )

assume A0: F is nonnegative ; :: thesis: ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )

set FF = Ser F;

defpred S

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

A1: (Ser F) . (0 + 1) = y + (F . 1) by Def11;

A2: for k being Nat st S

S

proof

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

assume that

A3: (Ser F) . k <= (Ser F) . (k + 1) and

A4: 0. <= (Ser F) . k ; :: thesis: S_{1}[k + 1]

(Ser F) . ((k + 1) + 1) = ((Ser F) . (k + 1)) + (F . ((k + 1) + 1)) by Def11;

hence S_{1}[k + 1]
by A3, A4, Th38, A0, XXREAL_3:39; :: thesis: verum

end;assume that

A3: (Ser F) . k <= (Ser F) . (k + 1) and

A4: 0. <= (Ser F) . k ; :: thesis: S

(Ser F) . ((k + 1) + 1) = ((Ser F) . (k + 1)) + (F . ((k + 1) + 1)) by Def11;

hence S

then A6: S

for n being Nat holds S

hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) ; :: thesis: verum