defpred S₁[ Nat] means ex f being FinSequence of F₃() st
( len f = $1 & F₁() = f . 1 & F₂() = f . (len f) & rng f c= rng F₄() & ( for i being Element of NAT st 1 <= i & i < len f holds
P₁[f . i,f . (i + 1)] ) );
for i being Element of NAT st 1 <= i & i < len F₄() holds
P₁[F₄() . i,F₄() . (i + 1)] by A2;
then A3: ex k being Nat st S₁[k] by A1;
consider k being Nat such that
A4: ( S₁[k] & ( for n being Nat st S₁[n] holds
k <= n ) ) from NAT_1:sch 5(A3);
consider g being FinSequence of F₃() such that
A5: len g = k and
A6: F₁() = g . 1 and
A7: F₂() = g . (len g) and
A8: rng g c= rng F₄() and
A9: for i being Element of NAT st 1 <= i & i < len g holds
P₁[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 A10, A11;

per cases ( x < y or y < x ) by A13, XXREAL_0:1;

suppose A14: x < y ; :: thesis: contradiction

set 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 F₄() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds
P₁[(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 F₄() by A8; :: thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(x + 1),y)) holds
P₁[(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 P₁[(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: P₁[(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: P₁[(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 P₁[(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: P₁[(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 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 P₁[(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: P₁[(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 P₁[(Del (g,(x + 1),y)) . i,(Del (g,(x + 1),y)) . (i + 1)] by A9, A37, A36, NAT_1:11; :: thesis: verum

end;

end;

end;

A38: F₂() = (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: F₂() = (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 A11, A19, Th3;
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 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 F₂() = (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: F₂() = (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
.= F₂() by A7 ;
:: thesis: verum

end;

end;

end;

1 <= (x + 1) - 1 by A10, FINSEQ_3:25;
then A44: F₁() = (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; :: thesis: verum

end;

suppose A45: y < x ; :: thesis: contradiction

set 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 F₄() & ( for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds
P₁[(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 F₄() by A8; :: thesis: for i being Element of NAT st 1 <= i & i < len (Del (g,(y + 1),x)) holds
P₁[(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 P₁[(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: P₁[(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: P₁[(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 P₁[(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: P₁[(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 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 P₁[(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: P₁[(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 P₁[(Del (g,(y + 1),x)) . i,(Del (g,(y + 1),x)) . (i + 1)] by A9, A68, A67, NAT_1:11; :: thesis: verum

end;

end;

end;

A69: F₂() = (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: F₂() = (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 A10, A50, Th3;
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 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 F₂() = (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: F₂() = (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
.= F₂() by A7 ;
:: thesis: verum

end;

end;

end;

1 <= (y + 1) - 1 by A11, FINSEQ_3:25;
then A75: F₁() = (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; :: thesis: verum

end;

end;

end;

hence ex g being one-to-one FinSequence of F₃() st
( F₁() = g . 1 & F₂() = g . (len g) & rng g c= rng F₄() & ( for j being Element of NAT st 1 <= j & j < len g holds
P₁[g . j,g . (j + 1)] ) ) by A6, A7, A8, A9; :: thesis: verum