let n, i, j be Element of NAT ; :: thesis: ( i <= n & j <= n implies ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) )

assume that

A1: i <= n and

A2: j <= n ; :: thesis: ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ; :: thesis: verum

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) )

assume that

A1: i <= n and

A2: j <= n ; :: thesis: ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

now :: thesis: ( ( i < j & ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) or ( i = j & ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) or ( j < i & ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) )end;

hence
ex fs1 being FinSequence of NAT st ( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) or ( i = j & ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) or ( j < i & ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ) )

per cases
( i < j or i = j or j < i )
by XXREAL_0:1;

end;

case A3:
i < j
; :: thesis: ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

then
i - j < j - j
by XREAL_1:9;

then A4: i -' j = 0 by XREAL_0:def 2;

j - i > 0 by A3, XREAL_1:50;

then A5: (j - i) + 1 > 0 + 1 by XREAL_1:6;

then (j + 1) - i >= 0 ;

then A6: (j + 1) -' i = (j - i) + 1 by XREAL_0:def 2;

then A7: (i + ((j + 1) -' i)) -' 1 = (i + ((j + 1) -' i)) - 1 by XREAL_0:def 2;

deffunc H_{1}( Nat) -> Element of NAT = (i + $1) -' 1;

ex p being FinSequence st

( len p = (j + 1) -' i & ( for k being Nat st k in dom p holds

p . k = H_{1}(k) ) )
from FINSEQ_1:sch 2();

then consider p being FinSequence such that

A8: len p = (j + 1) -' i and

A9: for k being Nat st k in dom p holds

p . k = (i + k) -' 1 ;

j - i >= i - i by A3, XREAL_1:9;

then A10: len p = ((i -' j) + (j -' i)) + 1 by A8, A6, A4, XREAL_0:def 2;

A11: (j + 1) -' i = (j + 1) - i by A5, XREAL_0:def 2;

then 1 in dom p by A5, A8, FINSEQ_3:25;

then p . 1 = (i + 1) -' 1 by A9;

then A12: p . 1 = i by NAT_D:34;

rng p c= NAT

A16: for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds

fs2 . i1 = (fs2 /. (i1 + 1)) + 1

k1 <= n

then p . (len p) = j by A8, A9, A11, A7;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A23, A12, A10, A16; :: thesis: verum

end;then A4: i -' j = 0 by XREAL_0:def 2;

j - i > 0 by A3, XREAL_1:50;

then A5: (j - i) + 1 > 0 + 1 by XREAL_1:6;

then (j + 1) - i >= 0 ;

then A6: (j + 1) -' i = (j - i) + 1 by XREAL_0:def 2;

then A7: (i + ((j + 1) -' i)) -' 1 = (i + ((j + 1) -' i)) - 1 by XREAL_0:def 2;

deffunc H

ex p being FinSequence st

( len p = (j + 1) -' i & ( for k being Nat st k in dom p holds

p . k = H

then consider p being FinSequence such that

A8: len p = (j + 1) -' i and

A9: for k being Nat st k in dom p holds

p . k = (i + k) -' 1 ;

j - i >= i - i by A3, XREAL_1:9;

then A10: len p = ((i -' j) + (j -' i)) + 1 by A8, A6, A4, XREAL_0:def 2;

A11: (j + 1) -' i = (j + 1) - i by A5, XREAL_0:def 2;

then 1 in dom p by A5, A8, FINSEQ_3:25;

then p . 1 = (i + 1) -' 1 by A9;

then A12: p . 1 = i by NAT_D:34;

rng p c= NAT

proof

then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in NAT )

assume x in rng p ; :: thesis: x in NAT

then consider y being object such that

A13: y in dom p and

A14: p . y = x by FUNCT_1:def 3;

y in Seg (len p) by A13, FINSEQ_1:def 3;

then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;

then consider k being Nat such that

A15: k = y and

1 <= k and

k <= len p ;

p . k = (i + k) -' 1 by A9, A13, A15;

hence x in NAT by A14, A15; :: thesis: verum

end;assume x in rng p ; :: thesis: x in NAT

then consider y being object such that

A13: y in dom p and

A14: p . y = x by FUNCT_1:def 3;

y in Seg (len p) by A13, FINSEQ_1:def 3;

then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;

then consider k being Nat such that

A15: k = y and

1 <= k and

k <= len p ;

p . k = (i + k) -' 1 by A9, A13, A15;

hence x in NAT by A14, A15; :: thesis: verum

A16: for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds

fs2 . i1 = (fs2 /. (i1 + 1)) + 1

proof

A23:
for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
let i1 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

assume that

A17: 1 <= i1 and

A18: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

A19: 1 <= 1 + i1 by NAT_1:11;

i1 + 1 <= len fs2 by A18, NAT_1:13;

then i1 + 1 in dom p by A19, FINSEQ_3:25;

then A20: fs2 . (i1 + 1) = (i + (i1 + 1)) -' 1 by A9;

1 + (i + i1) >= 1 by NAT_1:11;

then (1 + (i + i1)) - 1 >= 1 - 1 by XREAL_1:9;

then A21: (1 + (i + i1)) -' 1 = i + i1 by XREAL_0:def 2;

i + i1 >= 1 + 0 by A17, XREAL_1:7;

then (i + i1) - 1 >= 1 - 1 by XREAL_1:9;

then A22: 1 + ((i + i1) -' 1) = 1 + ((i + i1) - 1) by XREAL_0:def 2

.= i + i1 ;

( i1 in dom fs2 & fs2 /. i1 = fs2 . i1 ) by A17, A18, FINSEQ_3:25, FINSEQ_4:15;

hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A9, A20, A22, A21; :: thesis: verum

end;assume that

A17: 1 <= i1 and

A18: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

A19: 1 <= 1 + i1 by NAT_1:11;

i1 + 1 <= len fs2 by A18, NAT_1:13;

then i1 + 1 in dom p by A19, FINSEQ_3:25;

then A20: fs2 . (i1 + 1) = (i + (i1 + 1)) -' 1 by A9;

1 + (i + i1) >= 1 by NAT_1:11;

then (1 + (i + i1)) - 1 >= 1 - 1 by XREAL_1:9;

then A21: (1 + (i + i1)) -' 1 = i + i1 by XREAL_0:def 2;

i + i1 >= 1 + 0 by A17, XREAL_1:7;

then (i + i1) - 1 >= 1 - 1 by XREAL_1:9;

then A22: 1 + ((i + i1) -' 1) = 1 + ((i + i1) - 1) by XREAL_0:def 2

.= i + i1 ;

( i1 in dom fs2 & fs2 /. i1 = fs2 . i1 ) by A17, A18, FINSEQ_3:25, FINSEQ_4:15;

hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A9, A20, A22, A21; :: thesis: verum

k1 <= n

proof

len p in dom p
by A5, A8, A11, FINSEQ_3:25;
let k, k1 be Element of NAT ; :: thesis: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )

assume that

A24: 1 <= k and

A25: k <= len p and

A26: k1 = p . k ; :: thesis: k1 <= n

k in dom p by A24, A25, FINSEQ_3:25;

then A27: k1 = (k + i) -' 1 by A9, A26;

(k + i) - 1 = k + (i - 1) ;

then 1 + (i - 1) <= (k + i) - 1 by A24, XREAL_1:6;

then A28: k1 = (k + i) - 1 by A27, XREAL_0:def 2;

k + i <= ((j + 1) -' i) + i by A8, A25, XREAL_1:6;

then k + i <= ((j + 1) - i) + i by A5, XREAL_0:def 2;

then k1 <= (j + 1) - 1 by A28, XREAL_1:9;

hence k1 <= n by A2, XXREAL_0:2; :: thesis: verum

end;assume that

A24: 1 <= k and

A25: k <= len p and

A26: k1 = p . k ; :: thesis: k1 <= n

k in dom p by A24, A25, FINSEQ_3:25;

then A27: k1 = (k + i) -' 1 by A9, A26;

(k + i) - 1 = k + (i - 1) ;

then 1 + (i - 1) <= (k + i) - 1 by A24, XREAL_1:6;

then A28: k1 = (k + i) - 1 by A27, XREAL_0:def 2;

k + i <= ((j + 1) -' i) + i by A8, A25, XREAL_1:6;

then k + i <= ((j + 1) - i) + i by A5, XREAL_0:def 2;

then k1 <= (j + 1) - 1 by A28, XREAL_1:9;

hence k1 <= n by A2, XXREAL_0:2; :: thesis: verum

then p . (len p) = j by A8, A9, A11, A7;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A23, A12, A10, A16; :: thesis: verum

case A29:
i = j
; :: thesis: ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

then
i - j = 0
;

then A30: i -' j = 0 by XREAL_0:def 2;

consider f being Function such that

A31: dom f = Seg 1 and

A32: rng f = {i} by FUNCT_1:5;

( rng f c= NAT & f is FinSequence-like ) by A31, A32, FINSEQ_1:def 2, ZFMISC_1:31;

then reconsider fs1 = f as FinSequence of NAT by FINSEQ_1:def 4;

A33: for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 by A31, FINSEQ_1:def 3;

1 in dom f by A31, FINSEQ_1:1;

then fs1 . 1 in rng f by FUNCT_1:def 3;

then A34: fs1 . 1 = i by A32, TARSKI:def 1;

A35: len fs1 = 1 by A31, FINSEQ_1:def 3;

then for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n by A1, A34, XXREAL_0:1;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A29, A34, A35, A30, A33; :: thesis: verum

end;then A30: i -' j = 0 by XREAL_0:def 2;

consider f being Function such that

A31: dom f = Seg 1 and

A32: rng f = {i} by FUNCT_1:5;

( rng f c= NAT & f is FinSequence-like ) by A31, A32, FINSEQ_1:def 2, ZFMISC_1:31;

then reconsider fs1 = f as FinSequence of NAT by FINSEQ_1:def 4;

A33: for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 by A31, FINSEQ_1:def 3;

1 in dom f by A31, FINSEQ_1:1;

then fs1 . 1 in rng f by FUNCT_1:def 3;

then A34: fs1 . 1 = i by A32, TARSKI:def 1;

A35: len fs1 = 1 by A31, FINSEQ_1:def 3;

then for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n by A1, A34, XXREAL_0:1;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A29, A34, A35, A30, A33; :: thesis: verum

case A36:
j < i
; :: thesis: ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

then A37:
i - j >= j - j
by XREAL_1:9;

j - i < i - i by A36, XREAL_1:9;

then j -' i = 0 by XREAL_0:def 2;

then A39: ((i -' j) + (j -' i)) + 1 = ((i - j) + 1) + (j -' i) by A37, XREAL_0:def 2

.= (i + 1) - j by A38 ;

deffunc H_{1}( Nat) -> Element of NAT = (i + 1) -' $1;

A40: (i + 1) - 1 >= 0 ;

i - j > 0 by A36, XREAL_1:50;

then A41: (i - j) + 1 > 0 + 1 by XREAL_1:6;

then A42: (i + 1) - ((i + 1) -' j) = (i + 1) - ((i + 1) - j) by XREAL_0:def 2

.= j ;

ex p being FinSequence st

( len p = (i + 1) -' j & ( for k being Nat st k in dom p holds

p . k = H_{1}(k) ) )
from FINSEQ_1:sch 2();

then consider p being FinSequence such that

A43: len p = (i + 1) -' j and

A44: for k being Nat st k in dom p holds

p . k = (i + 1) -' k ;

A45: (i + 1) -' j = (i + 1) - j by A41, XREAL_0:def 2;

then 1 in dom p by A41, A43, FINSEQ_3:25;

then p . 1 = (i + 1) -' 1 by A44;

then A46: p . 1 = i by A40, XREAL_0:def 2;

rng p c= NAT

(i - j) + 1 >= 0 + 1 by A37, XREAL_1:6;

then A51: (i + 1) - j >= 0 ;

A52: for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds

fs2 . i1 = (fs2 /. (i1 + 1)) + 1

k1 <= n

then p . (len p) = (i + 1) -' ((i + 1) -' j) by A43, A44

.= j by A42, XREAL_0:def 2 ;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A43, A59, A45, A46, A39, A52; :: thesis: verum

end;j - i < i - i by A36, XREAL_1:9;

then j -' i = 0 by XREAL_0:def 2;

then A39: ((i -' j) + (j -' i)) + 1 = ((i - j) + 1) + (j -' i) by A37, XREAL_0:def 2

.= (i + 1) - j by A38 ;

deffunc H

A40: (i + 1) - 1 >= 0 ;

i - j > 0 by A36, XREAL_1:50;

then A41: (i - j) + 1 > 0 + 1 by XREAL_1:6;

then A42: (i + 1) - ((i + 1) -' j) = (i + 1) - ((i + 1) - j) by XREAL_0:def 2

.= j ;

ex p being FinSequence st

( len p = (i + 1) -' j & ( for k being Nat st k in dom p holds

p . k = H

then consider p being FinSequence such that

A43: len p = (i + 1) -' j and

A44: for k being Nat st k in dom p holds

p . k = (i + 1) -' k ;

A45: (i + 1) -' j = (i + 1) - j by A41, XREAL_0:def 2;

then 1 in dom p by A41, A43, FINSEQ_3:25;

then p . 1 = (i + 1) -' 1 by A44;

then A46: p . 1 = i by A40, XREAL_0:def 2;

rng p c= NAT

proof

then reconsider fs2 = p as FinSequence of NAT by FINSEQ_1:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in NAT )

assume x in rng p ; :: thesis: x in NAT

then consider y being object such that

A47: y in dom p and

A48: p . y = x by FUNCT_1:def 3;

y in Seg (len p) by A47, FINSEQ_1:def 3;

then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;

then consider k being Nat such that

A49: k = y and

A50: ( 1 <= k & k <= len p ) ;

k in dom p by A50, FINSEQ_3:25;

then p . k = (i + 1) -' k by A44;

hence x in NAT by A48, A49; :: thesis: verum

end;assume x in rng p ; :: thesis: x in NAT

then consider y being object such that

A47: y in dom p and

A48: p . y = x by FUNCT_1:def 3;

y in Seg (len p) by A47, FINSEQ_1:def 3;

then y in { k where k is Nat : ( 1 <= k & k <= len p ) } by FINSEQ_1:def 1;

then consider k being Nat such that

A49: k = y and

A50: ( 1 <= k & k <= len p ) ;

k in dom p by A50, FINSEQ_3:25;

then p . k = (i + 1) -' k by A44;

hence x in NAT by A48, A49; :: thesis: verum

(i - j) + 1 >= 0 + 1 by A37, XREAL_1:6;

then A51: (i + 1) - j >= 0 ;

A52: for i1 being Element of NAT st 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 holds

fs2 . i1 = (fs2 /. (i1 + 1)) + 1

proof

A59:
for k, k1 being Element of NAT st 1 <= k & k <= len p & k1 = p . k holds
let i1 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 < len fs2 & not fs2 . (i1 + 1) = (fs2 /. i1) + 1 implies fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

assume that

A53: 1 <= i1 and

A54: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

A55: i1 + 1 <= len fs2 by A54, NAT_1:13;

then i1 + 1 <= (i - j) + 1 by A43, A51, XREAL_0:def 2;

then i1 <= i - j by XREAL_1:6;

then i1 + j <= i by XREAL_1:19;

then j <= i - i1 by XREAL_1:19;

then A56: 1 + ((i + 1) -' (i1 + 1)) = 1 + ((i + 1) - (i1 + 1)) by XREAL_0:def 2

.= (i + 1) - i1 ;

A57: 1 <= i1 + 1 by A53, NAT_1:13;

then i1 + 1 in dom fs2 by A55, FINSEQ_3:25;

then fs2 . (i1 + 1) = (i + 1) -' (i1 + 1) by A44;

then A58: (fs2 /. (i1 + 1)) + 1 = 1 + ((i + 1) -' (i1 + 1)) by A57, A55, FINSEQ_4:15;

i1 in dom fs2 by A53, A54, FINSEQ_3:25;

then fs2 . i1 = (i + 1) -' i1 by A44;

hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A58, A56, XREAL_0:def 2; :: thesis: verum

end;assume that

A53: 1 <= i1 and

A54: i1 < len fs2 ; :: thesis: ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 )

A55: i1 + 1 <= len fs2 by A54, NAT_1:13;

then i1 + 1 <= (i - j) + 1 by A43, A51, XREAL_0:def 2;

then i1 <= i - j by XREAL_1:6;

then i1 + j <= i by XREAL_1:19;

then j <= i - i1 by XREAL_1:19;

then A56: 1 + ((i + 1) -' (i1 + 1)) = 1 + ((i + 1) - (i1 + 1)) by XREAL_0:def 2

.= (i + 1) - i1 ;

A57: 1 <= i1 + 1 by A53, NAT_1:13;

then i1 + 1 in dom fs2 by A55, FINSEQ_3:25;

then fs2 . (i1 + 1) = (i + 1) -' (i1 + 1) by A44;

then A58: (fs2 /. (i1 + 1)) + 1 = 1 + ((i + 1) -' (i1 + 1)) by A57, A55, FINSEQ_4:15;

i1 in dom fs2 by A53, A54, FINSEQ_3:25;

then fs2 . i1 = (i + 1) -' i1 by A44;

hence ( fs2 . (i1 + 1) = (fs2 /. i1) + 1 or fs2 . i1 = (fs2 /. (i1 + 1)) + 1 ) by A58, A56, XREAL_0:def 2; :: thesis: verum

k1 <= n

proof

len p in dom p
by A41, A43, A45, FINSEQ_3:25;
let k, k1 be Element of NAT ; :: thesis: ( 1 <= k & k <= len p & k1 = p . k implies k1 <= n )

assume that

A60: 1 <= k and

A61: k <= len p and

A62: k1 = p . k ; :: thesis: k1 <= n

k <= (i + 1) - j by A43, A60, A61, XREAL_0:def 2;

then k + j <= ((i + 1) - j) + j by XREAL_1:6;

then A63: (k + j) - k <= (i + 1) - k by XREAL_1:9;

- k <= - 1 by A60, XREAL_1:24;

then A64: (- k) + (i + 1) <= (- 1) + (i + 1) by XREAL_1:6;

k in dom p by A60, A61, FINSEQ_3:25;

then k1 = (i + 1) -' k by A44, A62;

then k1 = (i + 1) - k by A63, XREAL_0:def 2;

hence k1 <= n by A1, A64, XXREAL_0:2; :: thesis: verum

end;assume that

A60: 1 <= k and

A61: k <= len p and

A62: k1 = p . k ; :: thesis: k1 <= n

k <= (i + 1) - j by A43, A60, A61, XREAL_0:def 2;

then k + j <= ((i + 1) - j) + j by XREAL_1:6;

then A63: (k + j) - k <= (i + 1) - k by XREAL_1:9;

- k <= - 1 by A60, XREAL_1:24;

then A64: (- k) + (i + 1) <= (- 1) + (i + 1) by XREAL_1:6;

k in dom p by A60, A61, FINSEQ_3:25;

then k1 = (i + 1) -' k by A44, A62;

then k1 = (i + 1) - k by A63, XREAL_0:def 2;

hence k1 <= n by A1, A64, XXREAL_0:2; :: thesis: verum

then p . (len p) = (i + 1) -' ((i + 1) -' j) by A43, A44

.= j by A42, XREAL_0:def 2 ;

hence ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) by A43, A59, A45, A46, A39, A52; :: thesis: verum

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) ) ; :: thesis: verum