let R be FinSequence of REAL ; :: thesis: ( R is non-increasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m )
thus ( R is non-increasing implies for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ) :: thesis: ( ( for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ) implies R is non-increasing )

proof

defpred S₂[ Nat] means ( $1 in dom R implies for n being Element of NAT st n in dom R & n < $1 holds
R . n >= R . $1 );
assume A1: R is non-increasing ; :: thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m
A2: for m being Element of NAT st S₂[m] holds
S₂[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₂[m] implies S₂[m + 1] )
assume A3: S₂[m] ; :: thesis: S₂[m + 1]
assume A4: m + 1 in dom R ; :: thesis: for n being Element of NAT st n in dom R & n < m + 1 holds
R . n >= R . (m + 1)
then m + 1 <= len R by FINSEQ_3:25;
then A5: m <= len R by NAT_1:13;
let n be Element of NAT ; :: thesis: ( n in dom R & n < m + 1 implies R . n >= R . (m + 1) )
assume that
A6: n in dom R and
A7: n < m + 1 ; :: thesis: R . n >= R . (m + 1)
set t = R . m;
set r = R . n;
set s = R . (m + 1);
A8: n <= m by A7, NAT_1:13;
1 <= n by A6, FINSEQ_3:25;
then A9: 1 <= m by A8, XXREAL_0:2;
then A10: m in dom R by A5, FINSEQ_3:25;

now

per cases ( n = m or n <> m ) ;

case n = m ; :: thesis: R . n >= R . (m + 1)

hence R . n >= R . (m + 1) by A1, A4, A6, Def4; :: thesis: verum

end;

case n <> m ; :: thesis: R . n >= R . (m + 1)

then n < m by A8, XXREAL_0:1;
then A11: R . n >= R . m by A3, A6, A9, A5, FINSEQ_3:25;
R . m >= R . (m + 1) by A1, A4, A10, Def4;
hence R . n >= R . (m + 1) by A11, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence R . n >= R . (m + 1) ; :: thesis: verum

end;

Seg (len R) = dom R by FINSEQ_1:def 3;
then A12: S₂[ 0 ] by FINSEQ_1:1;
for m being Element of NAT holds S₂[m] from NAT_1:sch 1(A12, A2);
hence for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ; :: thesis: verum

end;

assume A13: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n >= R . m ; :: thesis: R is non-increasing
let n be Element of NAT ; :: according to RFINSEQ:def 3 :: thesis: ( n in dom R & n + 1 in dom R implies R . n >= R . (n + 1) )
A14: n < n + 1 by NAT_1:13;
assume ( n in dom R & n + 1 in dom R ) ; :: thesis: R . n >= R . (n + 1)
hence R . n >= R . (n + 1) by A13, A14; :: thesis: verum