defpred S1[ Nat] means ex f being FinSequence of F3() st
( len f = $1 & F1() = f . 1 & F2() = f . (len f) & rng f c= rng F4() & ( for i being Element of NAT st 1 <= i & i < len f holds
P1[f . i,f . (i + 1)] ) );
for i being Element of NAT st 1 <= i & i < len F4() holds
P1[F4() . i,F4() . (i + 1)]
by A2;
then A3:
ex k being Nat st S1[k]
by A1;
consider k being Nat such that
A4:
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) )
from NAT_1:sch 5(A3);
consider g being FinSequence of F3() such that
A5:
len g = k
and
A6:
F1() = g . 1
and
A7:
F2() = g . (len g)
and
A8:
rng g c= rng F4()
and
A9:
for i being Element of NAT st 1 <= i & i < len g holds
P1[g . i,g . (i + 1)]
by A4;
now g is one-to-one assume
not
g is
one-to-one
;
contradictionthen consider x,
y being
object such that A10:
x in dom g
and A11:
y in dom g
and A12:
g . x = g . y
and A13:
x <> y
by FUNCT_1:def 4;
reconsider x =
x,
y =
y as
Element of
NAT by A10, A11;
per cases
( x < y or y < x )
by A13, XXREAL_0:1;
suppose A14:
x < y
;
contradictionset d =
Del (
g,
(x + 1),
y);
A15:
1
<= y
by A11, FINSEQ_3:25;
A16:
x + 1
>= 1
by NAT_1:11;
A17:
y <= len g
by A11, FINSEQ_3:25;
then A18:
x < len g
by A14, XXREAL_0:2;
then
x + 1
<= len g
by NAT_1:13;
then A19:
x + 1
in dom g
by A16, FINSEQ_3:25;
A20:
x + 1
<= y
by A14, NAT_1:13;
then A21:
y - (x + 1) >= 0
by XREAL_1:48;
A22:
(
rng (Del (g,(x + 1),y)) c= rng F4() & ( for
i being
Element of
NAT st 1
<= i &
i < len (Del (g,(x + 1),y)) holds
P1[
(Del (g,(x + 1),y)) . i,
(Del (g,(x + 1),y)) . (i + 1)] ) )
proof
rng (Del (g,(x + 1),y)) c= rng g
by Th1;
hence
rng (Del (g,(x + 1),y)) c= rng F4()
by A8;
for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
let i be
Element of
NAT ;
( 1 <= i & i < len (Del (g,(x + 1),y)) implies P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] )
assume that A23:
1
<= i
and A24:
i < len (Del (g,(x + 1),y))
;
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
per cases
( i < x or i = x or i > x )
by XXREAL_0:1;
suppose A25:
i < x
;
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]then
i + 1
<= (x + 1) - 1
by NAT_1:13;
then A26:
(Del (g,(x + 1),y)) . (i + 1) = g . (i + 1)
by A19, Th4, NAT_1:11;
i <= (x + 1) - 1
by A25;
then A27:
(Del (g,(x + 1),y)) . i = g . i
by A19, A23, Th4;
i < len g
by A18, A25, XXREAL_0:2;
hence
P1[
(Del (g,(x + 1),y)) . i,
(Del (g,(x + 1),y)) . (i + 1)]
by A9, A23, A27, A26;
verum end; suppose A28:
i = x
;
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]then A29:
y < len g
by A17, XXREAL_0:1;
then A30:
0 < (len g) - y
by XREAL_1:50;
then
0 < (len g) -' y
by XREAL_0:def 2;
then
0 + 1
<= (len g) -' y
by NAT_1:13;
then
1
- 1
<= ((len g) -' y) - 1
by XREAL_1:9;
then
0 <= ((len g) - y) - 1
by A30, XREAL_0:def 2;
then
(i + 1) + 0 <= (i + 1) + (((len g) - y) - 1)
by XREAL_1:7;
then
(i + 1) + 0 <= ((i + 1) + ((len g) - y)) - 1
;
then A31:
(Del (g,(x + 1),y)) . (i + 1) =
g . (((y -' (x + 1)) + (i + 1)) + 1)
by A11, A20, A19, A28, Th6
.=
g . (y + 1)
by A20, A28, XREAL_1:235
;
i <= (x + 1) - 1
by A28;
then
(Del (g,(x + 1),y)) . i = g . y
by A12, A19, A23, A28, Th4;
hence
P1[
(Del (g,(x + 1),y)) . i,
(Del (g,(x + 1),y)) . (i + 1)]
by A9, A15, A29, A31;
verum end; suppose
i > x
;
P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]then A32:
x + 1
<= i
by NAT_1:13;
A33:
(len g) - y >= 0
by A17, XREAL_1:48;
i < (((len g) - y) + (x + 1)) - 1
by A11, A19, A24, Th2;
then A34:
i < (((len g) -' y) + (x + 1)) - 1
by A33, XREAL_0:def 2;
then
i + 1
<= ((len g) -' y) + x
by NAT_1:13;
then
i + 1
<= ((((len g) - y) + x) + 1) - 1
by A33, XREAL_0:def 2;
then A35:
i + 1
<= (((len g) - y) + (x + 1)) - 1
;
i < ((((len g) -' y) + x) + 1) - 1
by A34;
then
i < ((len g) - y) + x
by A33, XREAL_0:def 2;
then
i - x < (((len g) - y) + x) - x
by XREAL_1:9;
then
(i - x) + y < ((len g) - y) + y
by XREAL_1:8;
then
(((y - x) - 1) + i) + 1
< len g
;
then A36:
((y -' (x + 1)) + i) + 1
< len g
by A21, XREAL_0:def 2;
i <= i + 1
by NAT_1:11;
then
x + 1
<= i + 1
by A32, XXREAL_0:2;
then A37:
(Del (g,(x + 1),y)) . (i + 1) =
g . (((y -' (x + 1)) + (i + 1)) + 1)
by A11, A20, A19, A35, Th6
.=
g . ((((y -' (x + 1)) + i) + 1) + 1)
;
i <= (((len g) - y) + (x + 1)) - 1
by A11, A19, A24, Th2;
then
(Del (g,(x + 1),y)) . i = g . (((y -' (x + 1)) + i) + 1)
by A11, A20, A19, A32, Th6;
hence
P1[
(Del (g,(x + 1),y)) . i,
(Del (g,(x + 1),y)) . (i + 1)]
by A9, A37, A36, NAT_1:11;
verum end; end;
end; A38:
F2()
= (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
proof
per cases
( len (Del (g,(x + 1),y)) <= x or len (Del (g,(x + 1),y)) > x )
;
suppose A39:
len (Del (g,(x + 1),y)) <= x
;
F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))then A40:
0 + 1
<= len (Del (g,(x + 1),y))
by NAT_1:13;
len (Del (g,(x + 1),y)) <= (x + 1) - 1
by A39;
then A41:
(Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) = g . (len (Del (g,(x + 1),y)))
by A19, A40, Th4;
(((len g) - y) + (x + 1)) - 1
<= x
by A11, A19, A39, Th2;
then
((((len g) - y) + x) + 1) - 1
<= x
;
then
(len g) - y <= 0
by XREAL_1:29;
then
len g <= y
by XREAL_1:50;
then A42:
len g = y
by A17, XXREAL_0:1;
then
x <= (((len g) - y) + (x + 1)) - 1
;
hence
F2()
= (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
by A7, A11, A12, A19, A42, A41, Th2;
verum end; suppose
len (Del (g,(x + 1),y)) > x
;
F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))then A43:
x + 1
<= len (Del (g,(x + 1),y))
by NAT_1:13;
len (Del (g,(x + 1),y)) = (((len g) - y) + (x + 1)) - 1
by A11, A19, Th2;
hence (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y))) =
g . (((y -' (x + 1)) + ((((len g) - y) + (x + 1)) - 1)) + 1)
by A11, A20, A19, A43, Th6
.=
g . (((y - (x + 1)) + ((x + 1) + (((len g) - y) - 1))) + 1)
by A20, XREAL_1:233
.=
F2()
by A7
;
verum end; end;
end;
1
<= (x + 1) - 1
by A10, FINSEQ_3:25;
then A44:
F1()
= (Del (g,(x + 1),y)) . 1
by A6, A19, Th4;
0 < - (- (y - x))
by A14, XREAL_1:50;
then
- (y - x) < 0
;
then
(len g) + (- (y - x)) < (len g) + 0
by XREAL_1:8;
then
(((len g) - y) + (x + 1)) - 1
< len g
;
then
len (Del (g,(x + 1),y)) < len g
by A11, A19, Th2;
hence
contradiction
by A4, A5, A44, A38, A22;
verum end; suppose A45:
y < x
;
contradictionset d =
Del (
g,
(y + 1),
x);
A46:
1
<= x
by A10, FINSEQ_3:25;
A47:
y + 1
>= 1
by NAT_1:11;
A48:
x <= len g
by A10, FINSEQ_3:25;
then A49:
y < len g
by A45, XXREAL_0:2;
then
y + 1
<= len g
by NAT_1:13;
then A50:
y + 1
in dom g
by A47, FINSEQ_3:25;
A51:
y + 1
<= x
by A45, NAT_1:13;
then A52:
x - (y + 1) >= 0
by XREAL_1:48;
A53:
(
rng (Del (g,(y + 1),x)) c= rng F4() & ( for
i being
Element of
NAT st 1
<= i &
i < len (Del (g,(y + 1),x)) holds
P1[
(Del (g,(y + 1),x)) . i,
(Del (g,(y + 1),x)) . (i + 1)] ) )
proof
rng (Del (g,(y + 1),x)) c= rng g
by Th1;
hence
rng (Del (g,(y + 1),x)) c= rng F4()
by A8;
for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
let i be
Element of
NAT ;
( 1 <= i & i < len (Del (g,(y + 1),x)) implies P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] )
assume that A54:
1
<= i
and A55:
i < len (Del (g,(y + 1),x))
;
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
per cases
( i < y or i = y or i > y )
by XXREAL_0:1;
suppose A56:
i < y
;
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]then
i + 1
<= (y + 1) - 1
by NAT_1:13;
then A57:
(Del (g,(y + 1),x)) . (i + 1) = g . (i + 1)
by A50, Th4, NAT_1:11;
i <= (y + 1) - 1
by A56;
then A58:
(Del (g,(y + 1),x)) . i = g . i
by A50, A54, Th4;
i < len g
by A49, A56, XXREAL_0:2;
hence
P1[
(Del (g,(y + 1),x)) . i,
(Del (g,(y + 1),x)) . (i + 1)]
by A9, A54, A58, A57;
verum end; suppose A59:
i = y
;
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]then A60:
x < len g
by A48, XXREAL_0:1;
then A61:
0 < (len g) - x
by XREAL_1:50;
then
0 < (len g) -' x
by XREAL_0:def 2;
then
0 + 1
<= (len g) -' x
by NAT_1:13;
then
1
- 1
<= ((len g) -' x) - 1
by XREAL_1:9;
then
0 <= ((len g) - x) - 1
by A61, XREAL_0:def 2;
then
(i + 1) + 0 <= (i + 1) + (((len g) - x) - 1)
by XREAL_1:7;
then
(i + 1) + 0 <= ((i + 1) + ((len g) - x)) - 1
;
then A62:
(Del (g,(y + 1),x)) . (i + 1) =
g . (((x -' (y + 1)) + (i + 1)) + 1)
by A10, A51, A50, A59, Th6
.=
g . (x + 1)
by A51, A59, XREAL_1:235
;
i <= (y + 1) - 1
by A59;
then
(Del (g,(y + 1),x)) . i = g . x
by A12, A50, A54, A59, Th4;
hence
P1[
(Del (g,(y + 1),x)) . i,
(Del (g,(y + 1),x)) . (i + 1)]
by A9, A46, A60, A62;
verum end; suppose
i > y
;
P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]then A63:
y + 1
<= i
by NAT_1:13;
A64:
(len g) - x >= 0
by A48, XREAL_1:48;
i < (((len g) - x) + (y + 1)) - 1
by A10, A50, A55, Th2;
then A65:
i < (((len g) -' x) + (y + 1)) - 1
by A64, XREAL_0:def 2;
then
i + 1
<= ((len g) -' x) + y
by NAT_1:13;
then
i + 1
<= ((((len g) - x) + y) + 1) - 1
by A64, XREAL_0:def 2;
then A66:
i + 1
<= (((len g) - x) + (y + 1)) - 1
;
i < ((((len g) -' x) + y) + 1) - 1
by A65;
then
i < ((len g) - x) + y
by A64, XREAL_0:def 2;
then
i - y < (((len g) - x) + y) - y
by XREAL_1:9;
then
(i - y) + x < ((len g) - x) + x
by XREAL_1:8;
then
(((x - y) - 1) + i) + 1
< len g
;
then A67:
((x -' (y + 1)) + i) + 1
< len g
by A52, XREAL_0:def 2;
i <= i + 1
by NAT_1:11;
then
y + 1
<= i + 1
by A63, XXREAL_0:2;
then A68:
(Del (g,(y + 1),x)) . (i + 1) =
g . (((x -' (y + 1)) + (i + 1)) + 1)
by A10, A51, A50, A66, Th6
.=
g . ((((x -' (y + 1)) + i) + 1) + 1)
;
i <= (((len g) - x) + (y + 1)) - 1
by A10, A50, A55, Th2;
then
(Del (g,(y + 1),x)) . i = g . (((x -' (y + 1)) + i) + 1)
by A10, A51, A50, A63, Th6;
hence
P1[
(Del (g,(y + 1),x)) . i,
(Del (g,(y + 1),x)) . (i + 1)]
by A9, A68, A67, NAT_1:11;
verum end; end;
end; A69:
F2()
= (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
proof
per cases
( len (Del (g,(y + 1),x)) <= y or len (Del (g,(y + 1),x)) > y )
;
suppose A70:
len (Del (g,(y + 1),x)) <= y
;
F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))then A71:
0 + 1
<= len (Del (g,(y + 1),x))
by NAT_1:13;
len (Del (g,(y + 1),x)) <= (y + 1) - 1
by A70;
then A72:
(Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) = g . (len (Del (g,(y + 1),x)))
by A50, A71, Th4;
(((len g) - x) + (y + 1)) - 1
<= y
by A10, A50, A70, Th2;
then
((((len g) - x) + y) + 1) - 1
<= y
;
then
(len g) - x <= 0
by XREAL_1:29;
then
len g <= x
by XREAL_1:50;
then A73:
len g = x
by A48, XXREAL_0:1;
then
y <= (((len g) - x) + (y + 1)) - 1
;
hence
F2()
= (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
by A7, A10, A12, A50, A73, A72, Th2;
verum end; suppose
len (Del (g,(y + 1),x)) > y
;
F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))then A74:
y + 1
<= len (Del (g,(y + 1),x))
by NAT_1:13;
len (Del (g,(y + 1),x)) = (((len g) - x) + (y + 1)) - 1
by A10, A50, Th2;
hence (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x))) =
g . (((x -' (y + 1)) + ((((len g) - x) + (y + 1)) - 1)) + 1)
by A10, A51, A50, A74, Th6
.=
g . (((x - (y + 1)) + ((y + 1) + (((len g) - x) - 1))) + 1)
by A51, XREAL_1:233
.=
F2()
by A7
;
verum end; end;
end;
1
<= (y + 1) - 1
by A11, FINSEQ_3:25;
then A75:
F1()
= (Del (g,(y + 1),x)) . 1
by A6, A50, Th4;
0 < - (- (x - y))
by A45, XREAL_1:50;
then
- (x - y) < 0
;
then
(len g) + (- (x - y)) < (len g) + 0
by XREAL_1:8;
then
(((len g) - x) + (y + 1)) - 1
< len g
;
then
len (Del (g,(y + 1),x)) < len g
by A10, A50, Th2;
hence
contradiction
by A4, A5, A75, A69, A53;
verum end; end; end;
hence
ex g being one-to-one FinSequence of F3() st
( F1() = g . 1 & F2() = g . (len g) & rng g c= rng F4() & ( for j being Element of NAT st 1 <= j & j < len g holds
P1[g . j,g . (j + 1)] ) )
by A6, A7, A8, A9; verum