let R be FinSequence of REAL ; :: thesis: ( R is non-decreasing 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-decreasing 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-decreasing )

proof

assume A1: R is non-decreasing ; :: thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds
R . n <= R . m
defpred S₁[ Element of 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 );
A2: S₁[ 0 ] ;
A3: 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 A4: S₁[m] ; :: thesis: S₁[m + 1]
assume A5: 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)
let n be Element of NAT ; :: thesis: ( n in dom R & n < m + 1 implies R . n <= R . (m + 1) )
assume A6: ( n in dom R & n < m + 1 ) ; :: thesis: R . n <= R . (m + 1)
then A7: ( 1 <= m + 1 & m + 1 <= len R & 1 <= n & n <= len R & n <= m & m <= m + 1 ) by A5, FINSEQ_3:27, NAT_1:13;
then A8: ( 1 <= m & m <= len R ) by XXREAL_0:2;
then A9: m in dom R by FINSEQ_3:27;
set t = R . m;
set r = R . n;
set s = R . (m + 1);

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, A5, A6, INTEGRA2:def 1; :: thesis: verum

end;

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

then n < m by A7, XXREAL_0:1;
then A10: R . n <= R . m by A4, A6, A8, FINSEQ_3:27;
R . m <= R . (m + 1) by A1, A5, A9, INTEGRA2:def 1;
hence R . n <= R . (m + 1) by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
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 A11: 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-decreasing
let n be Element of NAT ; :: according to INTEGRA2:def 1 :: thesis: ( not n in dom R or not n + 1 in dom R or R . n <= R . (n + 1) )
assume A12: ( n in dom R & n + 1 in dom R ) ; :: thesis: R . n <= R . (n + 1)
n < n + 1 by NAT_1:13;
hence R . n <= R . (n + 1) by A11, A12; :: thesis: verum