let F be sequence of ExtREAL; :: thesis: ( F is nonnegative implies for n, k being Nat st n <= k holds
(Ser F) . n <= (Ser F) . k )
assume A1: F is nonnegative ; :: thesis: for n, k being Nat st n <= k holds
(Ser F) . n <= (Ser F) . k
let n, k be Nat; :: thesis: ( n <= k implies (Ser F) . n <= (Ser F) . k )
defpred S₁[ Nat] means (Ser F) . n <= (Ser F) . (n + $1);
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 A3: (Ser F) . n <= (Ser F) . (n + k) ; :: thesis: S₁[k + 1]
(Ser F) . (n + k) <= (Ser F) . ((n + k) + 1) by A1, SUPINF_2:40;
hence S₁[k + 1] by A3, XXREAL_0:2; :: thesis: verum

end;

assume n <= k ; :: thesis: (Ser F) . n <= (Ser F) . k
then consider s being Nat such that
A4: k = n + s by NAT_1:10;
A5: k = n + s by A4;
A6: S₁[ 0 ] ;
for s being Nat holds S₁[s] from NAT_1:sch 2(A6, A2);
hence (Ser F) . n <= (Ser F) . k by A5; :: thesis: verum