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 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 :: thesis: g is one-to-one
assume not g is one-to-one ; :: thesis: contradiction
then 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 ;
per cases ( x < y or y < x ) by ;
suppose A14: x < y ; :: thesis: contradiction
set d = Del (g,(x + 1),y);
A15: 1 <= y by ;
A16: x + 1 >= 1 by NAT_1:11;
A17: y <= len g by ;
then A18: x < len g by ;
then x + 1 <= len g by NAT_1:13;
then A19: x + 1 in dom g by ;
A20: x + 1 <= y by ;
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; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: 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 ;
i <= (x + 1) - 1 by A25;
then A27: (Del (g,(x + 1),y)) . i = g . i by ;
i < len g by ;
hence P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A23, A27, A26; :: thesis: verum
end;
suppose A28: i = x ; :: thesis: P1[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)]
now :: thesis: not y = len g
assume y = len g ; :: thesis: contradiction
then x < (((len g) - (len g)) + (x + 1)) - 1 by A11, A19, A24, A28, Th2;
hence contradiction ; :: thesis: verum
end;
then A29: y < len g by ;
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 ;
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 ;
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; :: thesis: verum
end;
suppose i > x ; :: thesis: 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 ;
i < (((len g) - y) + (x + 1)) - 1 by A11, A19, A24, Th2;
then A34: i < (((len g) -' y) + (x + 1)) - 1 by ;
then i + 1 <= ((len g) -' y) + x by NAT_1:13;
then i + 1 <= ((((len g) - y) + x) + 1) - 1 by ;
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 ;
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 ;
i <= i + 1 by NAT_1:11;
then x + 1 <= i + 1 by ;
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 ; :: thesis: 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 ; :: thesis: F2() = (Del (g,(x + 1),y)) . (len (Del (g,(x + 1),y)))
now :: thesis: not len (Del (g,(x + 1),y)) = 0
assume len (Del (g,(x + 1),y)) = 0 ; :: thesis: contradiction
then x + 1 = 0 + 1 by ;
hence contradiction by A10, FINSEQ_3:24; :: thesis: verum
end;
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 ;
(((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 ;
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; :: thesis: verum
end;
suppose len (Del (g,(x + 1),y)) > x ; :: thesis: 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 ;
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
.= F2() by A7 ;
:: thesis: verum
end;
end;
end;
1 <= (x + 1) - 1 by ;
then A44: F1() = (Del (g,(x + 1),y)) . 1 by A6, A19, Th4;
0 < - (- (y - x)) by ;
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 ;
hence contradiction by A4, A5, A44, A38, A22; :: thesis: verum
end;
suppose A45: y < x ; :: thesis: contradiction
set d = Del (g,(y + 1),x);
A46: 1 <= x by ;
A47: y + 1 >= 1 by NAT_1:11;
A48: x <= len g by ;
then A49: y < len g by ;
then y + 1 <= len g by NAT_1:13;
then A50: y + 1 in dom g by ;
A51: y + 1 <= x by ;
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; :: thesis: 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 ; :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: 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 ;
i <= (y + 1) - 1 by A56;
then A58: (Del (g,(y + 1),x)) . i = g . i by ;
i < len g by ;
hence P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A54, A58, A57; :: thesis: verum
end;
suppose A59: i = y ; :: thesis: P1[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)]
now :: thesis: not x = len g
assume x = len g ; :: thesis: contradiction
then y < (((len g) - (len g)) + (y + 1)) - 1 by A10, A50, A55, A59, Th2;
hence contradiction ; :: thesis: verum
end;
then A60: x < len g by ;
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 ;
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 ;
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; :: thesis: verum
end;
suppose i > y ; :: thesis: 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 ;
i < (((len g) - x) + (y + 1)) - 1 by A10, A50, A55, Th2;
then A65: i < (((len g) -' x) + (y + 1)) - 1 by ;
then i + 1 <= ((len g) -' x) + y by NAT_1:13;
then i + 1 <= ((((len g) - x) + y) + 1) - 1 by ;
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 ;
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 ;
i <= i + 1 by NAT_1:11;
then y + 1 <= i + 1 by ;
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 ; :: thesis: 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 ; :: thesis: F2() = (Del (g,(y + 1),x)) . (len (Del (g,(y + 1),x)))
now :: thesis: not len (Del (g,(y + 1),x)) = 0
assume len (Del (g,(y + 1),x)) = 0 ; :: thesis: contradiction
then y + 1 = 0 + 1 by ;
hence contradiction by A11, FINSEQ_3:24; :: thesis: verum
end;
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 ;
(((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 ;
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; :: thesis: verum
end;
suppose len (Del (g,(y + 1),x)) > y ; :: thesis: 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 ;
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
.= F2() by A7 ;
:: thesis: verum
end;
end;
end;
1 <= (y + 1) - 1 by ;
then A75: F1() = (Del (g,(y + 1),x)) . 1 by A6, A50, Th4;
0 < - (- (x - y)) by ;
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 ;
hence contradiction by A4, A5, A75, A69, A53; :: thesis: 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; :: thesis: verum