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 & F₁() = g . 1 & F₂() = g . (len g) & rng g c= rng F₄() & ( for i being Element of NAT st 1 <= i & i < len g holds
P₁[g . i,g . (i + 1)] ) ) by A4;

now

assume not g is one-to-one ; :: thesis: contradiction
then consider x, y being set such that
A6: ( x in dom g & y in dom g & g . x = g . y & x <> y ) by FUNCT_1:def 8;
reconsider x = x, y = y as Element of NAT by A6;

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

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

then A8: x + 1 <= y by NAT_1:13;
then A9: y - (x + 1) >= 0 by XREAL_1:50;
set d = Del g,(x + 1),y;
A10: x + 1 >= 1 by NAT_1:11;
A11: ( 1 <= y & y <= len g ) by A6, FINSEQ_3:27;
then A12: x < len g by A7, XXREAL_0:2;
then x + 1 <= len g by NAT_1:13;
then A13: x + 1 in dom g by A10, FINSEQ_3:27;
1 <= (x + 1) - 1 by A6, FINSEQ_3:27;
then A14: F₁() = (Del g,(x + 1),y) . 1 by A5, A13, Th4;
A15: 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 A16: len (Del g,(x + 1),y) <= x ; :: thesis: F₂() = (Del g,(x + 1),y) . (len (Del g,(x + 1),y))

then (((len g) - y) + (x + 1)) - 1 <= x by A6, A13, Th2;
then ((((len g) - y) + x) + 1) - 1 <= x ;
then (len g) - y <= 0 by XREAL_1:31;
then len g <= y by XREAL_1:52;
then A17: len g = y by A11, XXREAL_0:1;

now

assume len (Del g,(x + 1),y) = 0 ; :: thesis: contradiction
then x + 1 = 0 + 1 by A6, A13, Th3;
hence contradiction by A6, FINSEQ_3:26; :: thesis: verum

end;

then 0 < len (Del g,(x + 1),y) ;
then A18: 0 + 1 <= len (Del g,(x + 1),y) by NAT_1:13;
len (Del g,(x + 1),y) <= (x + 1) - 1 by A16;
then A19: (Del g,(x + 1),y) . (len (Del g,(x + 1),y)) = g . (len (Del g,(x + 1),y)) by A13, A18, Th4;
x <= (((len g) - y) + (x + 1)) - 1 by A17;
hence F₂() = (Del g,(x + 1),y) . (len (Del g,(x + 1),y)) by A5, A6, A13, A17, A19, Th2; :: thesis: verum

end;

suppose A20: len (Del g,(x + 1),y) > x ; :: thesis: F₂() = (Del g,(x + 1),y) . (len (Del g,(x + 1),y))

A21: len (Del g,(x + 1),y) = (((len g) - y) + (x + 1)) - 1 by A6, A13, Th2;
x + 1 <= len (Del g,(x + 1),y) by A20, NAT_1:13;
hence (Del g,(x + 1),y) . (len (Del g,(x + 1),y)) = g . (((y -' (x + 1)) + ((((len g) - y) + (x + 1)) - 1)) + 1) by A6, A8, A13, A21, Th6
.= g . (((y - (x + 1)) + ((x + 1) + (((len g) - y) - 1))) + 1) by A8, XREAL_1:235
.= F₂() by A5 ;
:: thesis: verum

end;

end;

end;

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 A5, XBOOLE_1:1; :: 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 A23: ( 1 <= i & 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 A24: i < x ; :: thesis: P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)]

then i <= (x + 1) - 1 ;
then A25: (Del g,(x + 1),y) . i = g . i by A13, A23, Th4;
i + 1 <= (x + 1) - 1 by A24, NAT_1:13;
then A26: (Del g,(x + 1),y) . (i + 1) = g . (i + 1) by A13, Th4, NAT_1:11;
i < len g by A12, A24, XXREAL_0:2;
hence P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)] by A5, A23, A25, A26; :: thesis: verum

end;

suppose A27: i = x ; :: thesis: P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)]

then i <= (x + 1) - 1 ;
then A28: (Del g,(x + 1),y) . i = g . y by A6, A13, A23, A27, Th4;

now

assume y = len g ; :: thesis: contradiction
then x < (((len g) - (len g)) + (x + 1)) - 1 by A6, A13, A23, A27, Th2;
hence contradiction ; :: thesis: verum

end;

then A29: y < len g by A11, XXREAL_0:1;
then A30: 0 < (len g) - y by XREAL_1:52;
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:11;
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:9;
then (i + 1) + 0 <= ((i + 1) + ((len g) - y)) - 1 ;
then (Del g,(x + 1),y) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A6, A8, A13, A27, Th6
.= g . (y + 1) by A8, A27, XREAL_1:237 ;
hence P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)] by A5, A11, A28, A29; :: thesis: verum

end;

suppose i > x ; :: thesis: P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)]

then A31: x + 1 <= i by NAT_1:13;
i <= (((len g) - y) + (x + 1)) - 1 by A6, A13, A23, Th2;
then A32: (Del g,(x + 1),y) . i = g . (((y -' (x + 1)) + i) + 1) by A6, A8, A13, A31, Th6;
i <= i + 1 by NAT_1:11;
then A33: x + 1 <= i + 1 by A31, XXREAL_0:2;
A34: (len g) - y >= 0 by A11, XREAL_1:50;
i < (((len g) - y) + (x + 1)) - 1 by A6, A13, A23, Th2;
then A35: i < (((len g) -' y) + (x + 1)) - 1 by A34, XREAL_0:def 2;
then A36: i < ((((len g) -' y) + x) + 1) - 1 ;
i + 1 <= ((len g) -' y) + x by A35, NAT_1:13;
then i + 1 <= ((((len g) - y) + x) + 1) - 1 by A34, XREAL_0:def 2;
then i + 1 <= (((len g) - y) + (x + 1)) - 1 ;
then A37: (Del g,(x + 1),y) . (i + 1) = g . (((y -' (x + 1)) + (i + 1)) + 1) by A6, A8, A13, A33, Th6
.= g . ((((y -' (x + 1)) + i) + 1) + 1) ;
i < ((len g) - y) + x by A34, A36, XREAL_0:def 2;
then i - x < (((len g) - y) + x) - x by XREAL_1:11;
then (i - x) + y < ((len g) - y) + y by XREAL_1:10;
then (((y - x) - 1) + i) + 1 < len g ;
then ((y -' (x + 1)) + i) + 1 < len g by A9, XREAL_0:def 2;
hence P₁[(Del g,(x + 1),y) . i,(Del g,(x + 1),y) . (i + 1)] by A5, A32, A37, NAT_1:11; :: thesis: verum

end;

end;

end;

0 < - (- (y - x)) by A7, XREAL_1:52;
then - (y - x) < 0 ;
then (len g) + (- (y - x)) < (len g) + 0 by XREAL_1:10;
then (((len g) - y) + (x + 1)) - 1 < len g ;
then len (Del g,(x + 1),y) < len g by A6, A13, Th2;
hence contradiction by A4, A5, A14, A15, A22; :: thesis: verum

end;

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

then A39: y + 1 <= x by NAT_1:13;
then A40: x - (y + 1) >= 0 by XREAL_1:50;
set d = Del g,(y + 1),x;
A41: y + 1 >= 1 by NAT_1:11;
A42: ( 1 <= x & x <= len g ) by A6, FINSEQ_3:27;
then A43: y < len g by A38, XXREAL_0:2;
then y + 1 <= len g by NAT_1:13;
then A44: y + 1 in dom g by A41, FINSEQ_3:27;
1 <= (y + 1) - 1 by A6, FINSEQ_3:27;
then A45: F₁() = (Del g,(y + 1),x) . 1 by A5, A44, Th4;
A46: 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 A47: len (Del g,(y + 1),x) <= y ; :: thesis: F₂() = (Del g,(y + 1),x) . (len (Del g,(y + 1),x))

then (((len g) - x) + (y + 1)) - 1 <= y by A6, A44, Th2;
then ((((len g) - x) + y) + 1) - 1 <= y ;
then (len g) - x <= 0 by XREAL_1:31;
then len g <= x by XREAL_1:52;
then A48: len g = x by A42, XXREAL_0:1;

now

assume len (Del g,(y + 1),x) = 0 ; :: thesis: contradiction
then y + 1 = 0 + 1 by A6, A44, Th3;
hence contradiction by A6, FINSEQ_3:26; :: thesis: verum

end;

then 0 < len (Del g,(y + 1),x) ;
then A49: 0 + 1 <= len (Del g,(y + 1),x) by NAT_1:13;
len (Del g,(y + 1),x) <= (y + 1) - 1 by A47;
then A50: (Del g,(y + 1),x) . (len (Del g,(y + 1),x)) = g . (len (Del g,(y + 1),x)) by A44, A49, Th4;
y <= (((len g) - x) + (y + 1)) - 1 by A48;
hence F₂() = (Del g,(y + 1),x) . (len (Del g,(y + 1),x)) by A5, A6, A44, A48, A50, Th2; :: thesis: verum

end;

suppose A51: len (Del g,(y + 1),x) > y ; :: thesis: F₂() = (Del g,(y + 1),x) . (len (Del g,(y + 1),x))

A52: len (Del g,(y + 1),x) = (((len g) - x) + (y + 1)) - 1 by A6, A44, Th2;
y + 1 <= len (Del g,(y + 1),x) by A51, NAT_1:13;
hence (Del g,(y + 1),x) . (len (Del g,(y + 1),x)) = g . (((x -' (y + 1)) + ((((len g) - x) + (y + 1)) - 1)) + 1) by A6, A39, A44, A52, Th6
.= g . (((x - (y + 1)) + ((y + 1) + (((len g) - x) - 1))) + 1) by A39, XREAL_1:235
.= F₂() by A5 ;
:: thesis: verum

end;

end;

end;

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 A5, XBOOLE_1:1; :: 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 A54: ( 1 <= i & 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 A55: i < y ; :: thesis: P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)]

then i <= (y + 1) - 1 ;
then A56: (Del g,(y + 1),x) . i = g . i by A44, A54, Th4;
i + 1 <= (y + 1) - 1 by A55, NAT_1:13;
then A57: (Del g,(y + 1),x) . (i + 1) = g . (i + 1) by A44, Th4, NAT_1:11;
i < len g by A43, A55, XXREAL_0:2;
hence P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)] by A5, A54, A56, A57; :: thesis: verum

end;

suppose A58: i = y ; :: thesis: P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)]

then i <= (y + 1) - 1 ;
then A59: (Del g,(y + 1),x) . i = g . x by A6, A44, A54, A58, Th4;

now

assume x = len g ; :: thesis: contradiction
then y < (((len g) - (len g)) + (y + 1)) - 1 by A6, A44, A54, A58, Th2;
hence contradiction ; :: thesis: verum

end;

then A60: x < len g by A42, XXREAL_0:1;
then A61: 0 < (len g) - x by XREAL_1:52;
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:11;
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:9;
then (i + 1) + 0 <= ((i + 1) + ((len g) - x)) - 1 ;
then (Del g,(y + 1),x) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A6, A39, A44, A58, Th6
.= g . (x + 1) by A39, A58, XREAL_1:237 ;
hence P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)] by A5, A42, A59, A60; :: thesis: verum

end;

suppose i > y ; :: thesis: P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)]

then A62: y + 1 <= i by NAT_1:13;
i <= (((len g) - x) + (y + 1)) - 1 by A6, A44, A54, Th2;
then A63: (Del g,(y + 1),x) . i = g . (((x -' (y + 1)) + i) + 1) by A6, A39, A44, A62, Th6;
i <= i + 1 by NAT_1:11;
then A64: y + 1 <= i + 1 by A62, XXREAL_0:2;
A65: (len g) - x >= 0 by A42, XREAL_1:50;
i < (((len g) - x) + (y + 1)) - 1 by A6, A44, A54, Th2;
then A66: i < (((len g) -' x) + (y + 1)) - 1 by A65, XREAL_0:def 2;
then A67: i < ((((len g) -' x) + y) + 1) - 1 ;
i + 1 <= ((len g) -' x) + y by A66, NAT_1:13;
then i + 1 <= ((((len g) - x) + y) + 1) - 1 by A65, XREAL_0:def 2;
then i + 1 <= (((len g) - x) + (y + 1)) - 1 ;
then A68: (Del g,(y + 1),x) . (i + 1) = g . (((x -' (y + 1)) + (i + 1)) + 1) by A6, A39, A44, A64, Th6
.= g . ((((x -' (y + 1)) + i) + 1) + 1) ;
i < ((len g) - x) + y by A65, A67, XREAL_0:def 2;
then i - y < (((len g) - x) + y) - y by XREAL_1:11;
then (i - y) + x < ((len g) - x) + x by XREAL_1:10;
then (((x - y) - 1) + i) + 1 < len g ;
then ((x -' (y + 1)) + i) + 1 < len g by A40, XREAL_0:def 2;
hence P₁[(Del g,(y + 1),x) . i,(Del g,(y + 1),x) . (i + 1)] by A5, A63, A68, NAT_1:11; :: thesis: verum

end;

end;

end;

0 < - (- (x - y)) by A38, XREAL_1:52;
then - (x - y) < 0 ;
then (len g) + (- (x - y)) < (len g) + 0 by XREAL_1:10;
then (((len g) - x) + (y + 1)) - 1 < len g ;
then len (Del g,(y + 1),x) < len g by A6, A44, Th2;
hence contradiction by A4, A5, A45, A46, 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 A5; :: thesis: verum