let A be FinSequence; ( 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 )
( ( 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 S1[
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
;
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
S1[
m] holds
S1[
m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A3:
S1[
m]
;
S1[m + 1]
let n be
Nat;
( 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
;
A . n c= A . (m + 1)
now ( ( 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
;
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;
verum end;
hence
A . n c= A . (m + 1)
;
verum
end;
let n,
m be
Nat;
( 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 )
;
A . n c= A . m
A12:
S1[
0 ]
;
for
m being
Nat holds
S1[
m]
from NAT_1:sch 2(A12, A2);
hence
A . n c= A . m
by A11;
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
; A is ascending
let n be Nat; REARRAN1:def 2 ( 1 <= n & n <= (len A) - 1 implies A . n c= A . (n + 1) )
assume that
A14:
1 <= n
and
A15:
n <= (len A) - 1
; 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; verum