let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for f being sequence of NAT st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) )
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; for f being sequence of NAT st f is bijective holds
( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) )
let f be sequence of NAT; ( f is bijective implies ( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) )
assume A1:
f is bijective
; ( ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) iff for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) )
hereby ( ( for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) ) ) implies for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) )
assume A2:
for
m,
n being
Element of
NAT holds
(
m <= n iff
f . m <= f . n,
S )
;
for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) )let k be
Element of
NAT ;
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) )
k <= k + 1
by NAT_1:11;
then
f . k <= f . (k + 1),
S
by A2;
then consider F being non
empty FinSequence of
NAT such that A3:
F /. 1
= f . k
and A4:
F /. (len F) = f . (k + 1)
and A5:
for
n being
Element of
NAT st 1
<= n &
n < len F holds
F /. (n + 1) in SUCC (
(F /. n),
S)
;
set F1 =
F -| (f . (k + 1));
set x =
(f . (k + 1)) .. F;
A6:
f . (k + 1) in rng F
by A4, FINSEQ_6:168;
then A7:
len (F -| (f . (k + 1))) = ((f . (k + 1)) .. F) - 1
by FINSEQ_4:34;
then A8:
(len (F -| (f . (k + 1)))) + 1
= (f . (k + 1)) .. F
;
A9:
(f . (k + 1)) .. F in dom F
by A6, FINSEQ_4:20;
then A10:
F /. ((len (F -| (f . (k + 1)))) + 1) =
F . ((f . (k + 1)) .. F)
by A7, PARTFUN1:def 6
.=
f . (k + 1)
by A6, FINSEQ_4:19
;
(f . (k + 1)) .. F <= len F
by A9, FINSEQ_3:25;
then A11:
len (F -| (f . (k + 1))) < len F
by A8, NAT_1:13;
1
<= len F
by NAT_1:14;
then A12:
1
in dom F
by FINSEQ_3:25;
then A13:
F /. 1
= F . 1
by PARTFUN1:def 6;
A14:
F . ((f . (k + 1)) .. F) = f . (k + 1)
by A6, FINSEQ_4:19;
A15:
dom f = NAT
by FUNCT_2:def 1;
A16:
f . k <> f . (k + 1)
then A17:
len (F -| (f . (k + 1))) <> 0
by A3, A14, A12, A7, PARTFUN1:def 6;
1
<= (f . (k + 1)) .. F
by A9, FINSEQ_3:25;
then
1
< (f . (k + 1)) .. F
by A3, A16, A14, A13, XXREAL_0:1;
then A18:
1
<= len (F -| (f . (k + 1)))
by A8, NAT_1:13;
reconsider F1 =
F -| (f . (k + 1)) as non
empty FinSequence of
NAT by A17, A6, FINSEQ_4:41;
rng f = NAT
by A1, FUNCT_2:def 3;
then consider m being
object such that A19:
m in dom f
and A20:
f . m = F /. (len F1)
by FUNCT_1:def 3;
reconsider m =
m as
Element of
NAT by A19;
A21:
len F1 in dom F
by A18, A11, FINSEQ_3:25;
A22:
len F1 in dom F1
by A18, FINSEQ_3:25;
then A23:
F1 /. (len F1) =
F1 . (len F1)
by PARTFUN1:def 6
.=
F . (len F1)
by A6, A22, FINSEQ_4:36
.=
F /. (len F1)
by A21, PARTFUN1:def 6
;
A24:
now not m = k + 1end; reconsider F2 =
<*(F /. (len F1)),(F /. ((f . (k + 1)) .. F))*> as non
empty FinSequence of
NAT ;
A28:
len F2 = 2
by FINSEQ_1:44;
then A29:
2
in dom F2
by FINSEQ_3:25;
then A30:
F2 /. (len F2) =
F2 . 2
by A28, PARTFUN1:def 6
.=
F /. ((f . (k + 1)) .. F)
by FINSEQ_1:44
.=
f . (k + 1)
by A14, A9, PARTFUN1:def 6
;
A31:
1
in dom F2
by A28, FINSEQ_3:25;
A32:
now for n being Element of NAT st 1 <= n & n < len F2 holds
F2 /. (n + 1) in SUCC ((F2 /. n),S)let n be
Element of
NAT ;
( 1 <= n & n < len F2 implies F2 /. (n + 1) in SUCC ((F2 /. n),S) )assume
( 1
<= n &
n < len F2 )
;
F2 /. (n + 1) in SUCC ((F2 /. n),S)then
(
n <> 0 &
n < 1
+ 1 )
by FINSEQ_1:44;
then
(
n <> 0 &
n <= 1 )
by NAT_1:13;
then A33:
n = 1
by NAT_1:25;
then A34:
F2 /. n =
F2 . 1
by A31, PARTFUN1:def 6
.=
F /. (len F1)
by FINSEQ_1:44
;
F2 /. (n + 1) =
F2 . 2
by A29, A33, PARTFUN1:def 6
.=
F /. ((len F1) + 1)
by A7, FINSEQ_1:44
;
hence
F2 /. (n + 1) in SUCC (
(F2 /. n),
S)
by A5, A18, A11, A34;
verum end; A35:
now for n being Element of NAT st 1 <= n & n < len F1 holds
F1 /. (n + 1) in SUCC ((F1 /. n),S)let n be
Element of
NAT ;
( 1 <= n & n < len F1 implies F1 /. (n + 1) in SUCC ((F1 /. n),S) )assume that A36:
1
<= n
and A37:
n < len F1
;
F1 /. (n + 1) in SUCC ((F1 /. n),S)A38:
1
<= n + 1
by A36, NAT_1:13;
A39:
n + 1
<= len F1
by A37, NAT_1:13;
then
n + 1
<= len F
by A11, XXREAL_0:2;
then A40:
n + 1
in dom F
by A38, FINSEQ_3:25;
n <= len F
by A11, A37, XXREAL_0:2;
then A41:
n in dom F
by A36, FINSEQ_3:25;
A42:
n in dom F1
by A36, A37, FINSEQ_3:25;
then A43:
F1 /. n =
F1 . n
by PARTFUN1:def 6
.=
F . n
by A6, A42, FINSEQ_4:36
.=
F /. n
by A41, PARTFUN1:def 6
;
A44:
n < len F
by A11, A37, XXREAL_0:2;
A45:
n + 1
in dom F1
by A38, A39, FINSEQ_3:25;
then F1 /. (n + 1) =
F1 . (n + 1)
by PARTFUN1:def 6
.=
F . (n + 1)
by A6, A45, FINSEQ_4:36
.=
F /. (n + 1)
by A40, PARTFUN1:def 6
;
hence
F1 /. (n + 1) in SUCC (
(F1 /. n),
S)
by A5, A36, A43, A44;
verum end; F2 /. 1 =
F2 . 1
by A31, PARTFUN1:def 6
.=
f . m
by A20, FINSEQ_1:44
;
then
f . m <= f . (k + 1),
S
by A30, A32;
then A46:
m <= k + 1
by A2;
A47:
1
in dom F1
by A18, FINSEQ_3:25;
then F1 /. 1 =
F1 . 1
by PARTFUN1:def 6
.=
F . 1
by A6, A47, FINSEQ_4:36
.=
f . k
by A3, A12, PARTFUN1:def 6
;
then
f . k <= f . m,
S
by A20, A23, A35;
then
k <= m
by A2;
then
(
m = k or
m = k + 1 )
by A46, NAT_1:9;
hence
f . (k + 1) in SUCC (
(f . k),
S)
by A5, A18, A11, A10, A20, A24;
for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= jlet j be
Element of
NAT ;
( f . j in SUCC ((f . k),S) implies k <= j )reconsider fk =
f . k,
fj =
f . j as
Element of
NAT ;
reconsider F =
<*fk,fj*> as non
empty FinSequence of
NAT ;
A48:
len F = 2
by FINSEQ_1:44;
then A49:
2
in dom F
by FINSEQ_3:25;
A50:
1
in dom F
by A48, FINSEQ_3:25;
then A51:
F /. 1 =
F . 1
by PARTFUN1:def 6
.=
f . k
by FINSEQ_1:44
;
assume A52:
f . j in SUCC (
(f . k),
S)
;
k <= jF /. (len F) =
F . 2
by A48, A49, PARTFUN1:def 6
.=
f . j
by FINSEQ_1:44
;
then
f . k <= f . j,
S
by A51, A53;
hence
k <= j
by A2;
verum
end;
assume A56:
for k being Element of NAT holds
( f . (k + 1) in SUCC ((f . k),S) & ( for j being Element of NAT st f . j in SUCC ((f . k),S) holds
k <= j ) )
; for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S )
let m, n be Element of NAT ; ( m <= n iff f . m <= f . n,S )
hereby ( f . m <= f . n,S implies m <= n )
assume A57:
m <= n
;
f . m <= f . n,Sper cases
( m = n or m < n )
by A57, XXREAL_0:1;
suppose A58:
m < n
;
f . m <= f . n,Sthus
f . m <= f . n,
S
verumproof
reconsider f9 =
f as
sequence of
NAT ;
set mn =
n -' m;
deffunc H1(
Nat)
-> Element of
NAT =
f9 . ((m + $1) -' 1);
consider F being
FinSequence of
NAT such that A59:
len F = (n -' m) + 1
and A60:
for
j being
Nat st
j in dom F holds
F . j = H1(
j)
from FINSEQ_2:sch 1();
reconsider F =
F as non
empty FinSequence of
NAT by A59;
take
F
;
AMI_WSTD:def 1 ( F /. 1 = f . m & F /. (len F) = f . n & ( for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ) )
A61:
1
<= (n -' m) + 1
by NAT_1:11;
then A62:
1
in dom F
by A59, FINSEQ_3:25;
hence F /. 1 =
F . 1
by PARTFUN1:def 6
.=
f . ((m + 1) -' 1)
by A60, A62
.=
f . m
by NAT_D:34
;
( F /. (len F) = f . n & ( for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S) ) )
m + 1
<= n
by A58, INT_1:7;
then
1
<= n - m
by XREAL_1:19;
then
0 <= n - m
;
then A63:
n -' m = n - m
by XREAL_0:def 2;
A64:
len F in dom F
by A59, A61, FINSEQ_3:25;
hence F /. (len F) =
F . (len F)
by PARTFUN1:def 6
.=
f . ((m + ((n -' m) + 1)) -' 1)
by A59, A60, A64
.=
f . (((m + (n -' m)) + 1) -' 1)
.=
f . n
by A63, NAT_D:34
;
for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S)
let p be
Element of
NAT ;
( 1 <= p & p < len F implies F /. (p + 1) in SUCC ((F /. p),S) )
assume that A65:
1
<= p
and A66:
p < len F
;
F /. (p + 1) in SUCC ((F /. p),S)
A67:
p in dom F
by A65, A66, FINSEQ_3:25;
then A68:
F /. p =
F . p
by PARTFUN1:def 6
.=
f . ((m + p) -' 1)
by A60, A67
;
A69:
p <= m + p
by NAT_1:11;
( 1
<= p + 1 &
p + 1
<= len F )
by A65, A66, NAT_1:13;
then A70:
p + 1
in dom F
by FINSEQ_3:25;
then F /. (p + 1) =
F . (p + 1)
by PARTFUN1:def 6
.=
f . ((m + (p + 1)) -' 1)
by A60, A70
.=
f . (((m + p) + 1) -' 1)
.=
f . (((m + p) -' 1) + 1)
by A65, A69, NAT_D:38, XXREAL_0:2
;
hence
F /. (p + 1) in SUCC (
(F /. p),
S)
by A56, A68;
verum
end; end;
end;
assume
f . m <= f . n,S
; m <= n
then consider F being non empty FinSequence of NAT such that
A71:
F /. 1 = f . m
and
A72:
F /. (len F) = f . n
and
A73:
for n being Element of NAT st 1 <= n & n < len F holds
F /. (n + 1) in SUCC ((F /. n),S)
;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len F implies ex l being Element of NAT st
( F /. $1 = f . l & m <= l ) );
A74:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A75:
S1[
k]
;
S1[k + 1]now ( 1 <= k + 1 & k + 1 <= len F implies ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l ) )assume that
1
<= k + 1
and A76:
k + 1
<= len F
;
ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l )per cases
( k = 0 or k > 0 )
;
suppose A77:
k > 0
;
ex l being Element of NAT st
( F /. (k + 1) = f . l & m <= l )
rng f = NAT
by A1, FUNCT_2:def 3;
then consider l1 being
object such that A78:
l1 in dom f
and A79:
f . l1 = F /. (k + 1)
by FUNCT_1:def 3;
consider l being
Element of
NAT such that A80:
F /. k = f . l
and A81:
m <= l
by A75, A76, A77, NAT_1:13, NAT_1:14;
reconsider l1 =
l1 as
Element of
NAT by A78;
reconsider kk =
k as
Element of
NAT by ORDINAL1:def 12;
k < len F
by A76, NAT_1:13;
then
F /. (kk + 1) in SUCC (
(F /. kk),
S)
by A73, A77, NAT_1:14;
then
l <= l1
by A56, A80, A79;
hence
ex
l being
Element of
NAT st
(
F /. (k + 1) = f . l &
m <= l )
by A81, A79, XXREAL_0:2;
verum end; end; hence
S1[
k + 1]
;
verum end;
A82:
1 <= len F
by NAT_1:14;
A83:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A83, A74);
then
( dom f = NAT & ex l being Element of NAT st
( F /. (len F) = f . l & m <= l ) )
by A82, FUNCT_2:def 1;
hence
m <= n
by A1, A72, FUNCT_1:def 4; verum