let A be FinSequence; :: thesis: ( A is ascending iff for n, m being Element of 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 Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) :: thesis: ( ( for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) implies A is ascending )

proof

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

now

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 A5, XXREAL_0:1;
then A6: n <= m by NAT_1:13;
A7: ( 1 <= n & m + 1 <= len A & m <= m + 1 ) by A5, FINSEQ_3:27, NAT_1:11;
then A8: ( 1 <= m & m <= len A ) by A6, XXREAL_0:2;
then m in dom A by FINSEQ_3:27;
then A9: A . n c= A . m by A4, A5, A6;
m <= (len A) - 1 by A7, XREAL_1:21;
then A . m c= A . (m + 1) by A1, A8, Def2;
hence A . n c= A . (m + 1) by A9, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

end;

A10: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A2, A3);
let n, m be Element of NAT ; :: thesis: ( n <= m & n in dom A & m in dom A implies A . n c= A . m )
assume ( n <= m & n in dom A & m in dom A ) ; :: thesis: A . n c= A . m
hence A . n c= A . m by A10; :: thesis: verum

end;

assume A11: for n, m being Element of 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 A12: ( 1 <= n & n <= (len A) - 1 ) ; :: thesis: A . n c= A . (n + 1)
then A13: ( n <= n + 1 & n + 1 <= len A ) by NAT_1:11, XREAL_1:21;
then ( 1 <= n + 1 & n <= len A ) by A12, XXREAL_0:2;
then ( n in dom A & n + 1 in dom A ) by A12, A13, FINSEQ_3:27;
hence A . n c= A . (n + 1) by A11, A13; :: thesis: verum