let R be real-valued FinSequence; :: thesis: ( R is non-decreasing iff for n, m being 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 Nat st n in dom R & m in dom R & n < m holds
R . n <= R . m ) :: thesis: ( ( for n, m being Nat st n in dom R & m in dom R & n < m holds
R . n <= R . m ) implies R is non-decreasing )

proof

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

proof

let m be 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 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 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 :: thesis: ( ( n = m & R . n <= R . (m + 1) ) or ( n <> m & R . n <= R . (m + 1) ) )

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; :: 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;
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;

A12: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A12, A2);
hence for n, m being 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 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 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) )
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