let s be positive Nat; :: thesis: for f being s -element natural-valued increasing positive-yielding FinSequence holds Sierp162FS_2 f is increasing
let f be s -element natural-valued increasing positive-yielding FinSequence; :: thesis: Sierp162FS_2 f is increasing
set g = Sierp162FS_2 f;
set F = 6 (#) f;
A1: f . 1 >= 0 + 1 by NAT_1:13;
(6 (#) f) . 1 = 6 * (f . 1) by VALUED_1:6;
then (6 (#) f) . 1 >= 6 * 1 by A1, XREAL_1:64;
then <*2,3*> . 2 < (6 (#) f) . 1 by XXREAL_0:2;
hence Sierp162FS_2 f is increasing by Lm22, Th38; :: thesis: verum