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₁[ 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₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A3: (Ser F) . k <= (Ser F) . (k + 1) and
A4: 0. <= (Ser F) . k ; :: thesis: S₁[k + 1]
(Ser F) . ((k + 1) + 1) = ((Ser F) . (k + 1)) + (F . ((k + 1) + 1)) by Def11;
hence S₁[k + 1] by A3, A4, Th38, A0, XXREAL_3:39; :: thesis: verum

end;

(Ser F) . 0 = F . 0 by Def11;
then A6: S₁[ 0 ] by A1, XXREAL_3:39, A0, Th38;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2);
hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) ; :: thesis: verum