let A be FinSequence; :: thesis: ( A is ascending iff for n, m being Nat st n <= m & n in dom A & m in dom A holds
A . n c= A . m )
thus ( A is ascending implies for n, m being Nat st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) :: thesis: ( ( for n, m being Nat st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) implies A is ascending )

proof

defpred S₁[ Nat] means for n being Nat st n <= $1 & n in dom A & $1 in dom A holds
A . n c= A . $1;
assume A1: A is ascending ; :: thesis: for n, m being Nat st n <= m & n in dom A & m in dom A holds
A . n c= A . 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]
let n be Nat; :: thesis: ( n <= m + 1 & n in dom A & m + 1 in dom A implies A . n c= A . (m + 1) )
assume that
A4: n <= m + 1 and
A5: n in dom A and
A6: m + 1 in dom A ; :: thesis: A . n c= A . (m + 1)

now :: thesis: ( ( n = m + 1 & A . n c= A . (m + 1) ) or ( n <> m + 1 & A . n c= A . (m + 1) ) )

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

case n = m + 1 ; :: thesis: A . n c= A . (m + 1)

hence A . n c= A . (m + 1) ; :: thesis: verum

end;

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

then n < m + 1 by A4, XXREAL_0:1;
then A7: n <= m by NAT_1:13;
1 <= n by A5, FINSEQ_3:25;
then A8: 1 <= m by A7, XXREAL_0:2;
A9: m + 1 <= len A by A6, FINSEQ_3:25;
m <= m + 1 by NAT_1:11;
then m <= len A by A9, XXREAL_0:2;
then m in dom A by A8, FINSEQ_3:25;
then A10: A . n c= A . m by A3, A5, A7;
m <= (len A) - 1 by A9, XREAL_1:19;
then A . m c= A . (m + 1) by A1, A8;
hence A . n c= A . (m + 1) by A10; :: thesis: verum

end;

end;

end;

hence A . n c= A . (m + 1) ; :: thesis: verum

end;

let n, m be Nat; :: thesis: ( n <= m & n in dom A & m in dom A implies A . n c= A . m )
assume A11: ( n <= m & n in dom A & m in dom A ) ; :: thesis: A . n c= A . m
A12: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A12, A2);
hence A . n c= A . m by A11; :: thesis: verum

end;

assume A13: for n, m being Nat st n <= m & n in dom A & m in dom A holds
A . n c= A . m ; :: thesis: A is ascending
let n be Nat; :: according to REARRAN1:def 2 :: thesis: ( 1 <= n & n <= (len A) - 1 implies A . n c= A . (n + 1) )
assume that
A14: 1 <= n and
A15: n <= (len A) - 1 ; :: thesis: A . n c= A . (n + 1)
A16: n + 1 <= len A by A15, XREAL_1:19;
n <= n + 1 by NAT_1:11;
then n <= len A by A16, XXREAL_0:2;
then A17: n in dom A by A14, FINSEQ_3:25;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom A by A16, FINSEQ_3:25;
hence A . n c= A . (n + 1) by A13, A17, NAT_1:11; :: thesis: verum