let v be FinSequence of REAL ; :: thesis: for n being Element of NAT st v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) holds
( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
let n be Element of NAT ; :: thesis: ( v <> {} & rng v c= Seg n & v . 1 = 1 & v . (len v) = n & ( for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ) implies ( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) ) )
assume that
A1: v <> {} and
A2: rng v c= Seg n and
A3: v . 1 = 1 and
A4: v . (len v) = n and
A5: for k being Element of NAT st 1 <= k & k <= (len v) - 1 holds
for r, s being Real st r = v . k & s = v . (k + 1) & not abs (r - s) = 1 holds
r = s ; :: thesis: ( ( for i being Element of NAT st i in Seg n holds
ex k being Element of NAT st
( k in dom v & v . k = i ) ) & ( for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r ) )
len v <> 0 by A1;
then 0 < len v ;
then A6: ( 1 <= 1 & 0 + 1 <= len v & len v <= len v ) by NAT_1:13;
then A7: ( 1 in dom v & len v in dom v ) by FINSEQ_3:27;
defpred S₁[ Element of NAT ] means ( $1 in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = $1 ) );
A8: S₁[ 0 ] by FINSEQ_1:3;
A9: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A10: ( i in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = i ) ) ; :: thesis: S₁[i + 1]
assume A11: i + 1 in Seg n ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

now

per cases ( i = 0 or i <> 0 ) ;

suppose A12: i = 0 ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

take k = 1; :: thesis: ( k in dom v & v . k = i + 1 )
thus ( k in dom v & v . k = i + 1 ) by A3, A6, A12, FINSEQ_3:27; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )

then 0 < i ;
then ( 0 + 1 <= i & i <= i + 1 & i + 1 <= n ) by A11, FINSEQ_1:3, NAT_1:13;
then A13: ( 1 <= i & i <= n ) by XXREAL_0:2;
then A14: i in Seg n by FINSEQ_1:3;
defpred S₂[ set ] means ( $1 in dom v & v . $1 = i );
A15: ex k being Nat st S₂[k] by A10, A13, FINSEQ_1:3;
A16: for k being Nat st S₂[k] holds
k <= len v by FINSEQ_3:27;
consider m being Nat such that
A17: ( S₂[m] & ( for k being Nat st S₂[k] holds
k <= m ) ) from NAT_1:sch 6(A16, A15);
A18: ( S₂[m] & ( for k being Element of NAT st S₂[k] holds
k <= m ) ) by A17;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
take k = m + 1; :: thesis: ( k in dom v & v . k = i + 1 )
thus ( k in dom v & v . k = i + 1 ) by A1, A2, A4, A5, A11, A14, A18, Th14; :: thesis: verum

end;

end;

end;

hence ex k being Element of NAT st
( k in dom v & v . k = i + 1 ) ; :: thesis: verum

end;

thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A8, A9); :: thesis: for m, k, i being Element of NAT
for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let m, k, i be Element of NAT ; :: thesis: for r being Real st m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k holds
i < r
let r be Real; :: thesis: ( m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k implies i < r )
assume A19: ( m in dom v & v . m = i & ( for j being Element of NAT st j in dom v & v . j = i holds
j <= m ) & m < k & k in dom v & r = v . k ) ; :: thesis: i < r
then A20: ( 1 <= m & m <= len v & 1 <= k & k <= len v ) by FINSEQ_3:27;
A21: i in rng v by A19, FUNCT_1:def 5;
then A22: ( 1 <= i & i <= n & i <= i + 1 ) by A2, FINSEQ_1:3, NAT_1:11;

now

per cases ( i = n or i <> n ) ;

suppose i = n ; :: thesis: i < r

then len v <= m by A4, A7, A19;
hence i < r by A19, A20, XXREAL_0:1; :: thesis: verum

end;

suppose i <> n ; :: thesis: i < r

then i < n by A22, XXREAL_0:1;
then ( 1 <= i + 1 & i + 1 <= n ) by NAT_1:11, NAT_1:13;
then i + 1 in Seg n by FINSEQ_1:3;
then A23: ( m + 1 in dom v & v . (m + 1) = i + 1 ) by A1, A2, A4, A5, A19, A21, Th14;
defpred S₂[ set ] means for j being Element of NAT
for s being Real st j = $1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s;
A24: S₂[ 0 ] ;
A25: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A26: S₂[k] ; :: thesis: S₂[k + 1]
let j be Element of NAT ; :: thesis: for s being Real st j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) holds
i < s
let s be Real; :: thesis: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) implies i < s )
assume A27: ( j = k + 1 & j > 0 & m + j in dom v & s = v . (m + j) ) ; :: thesis: i < s

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: i < s

hence i < s by A23, A27, NAT_1:13; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: i < s

then A28: ( 0 < k & m + (k + 1) <= len v & (m + k) + 1 = m + (k + 1) & m + k <= (m + k) + 1 & m <= m + k ) by A27, FINSEQ_3:27, NAT_1:11;
then A29: ( 1 <= m + k & m + k <= len v & m + k <= (len v) - 1 ) by A20, XREAL_1:21, XXREAL_0:2;
then A30: m + k in dom v by FINSEQ_3:27;
then v . (m + k) in rng v by FUNCT_1:def 5;
then ( v . (m + k) in Seg n & Seg n c= NAT ) by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
s in rng v by A27, FUNCT_1:def 5;
then ( s in Seg n & Seg n c= NAT ) by A2;
then reconsider s1 = s as Element of NAT ;
A31: i < r1 by A26, A28, A30;

now

per cases ( abs (r1 - s) = 1 or r1 = s ) by A5, A27, A28, A29;

suppose A32: abs (r1 - s) = 1 ; :: thesis: i < s

now

per cases ( ( r1 > s & r1 = s + 1 ) or ( r1 < s & s = r1 + 1 ) ) by A32, Th1;

suppose ( r1 > s & r1 = s + 1 ) ; :: thesis: i < s

then A33: i <= s1 by A31, NAT_1:13;

now

per cases ( i < s or s = i ) by A33, XXREAL_0:1;

case i < s ; :: thesis: i < s

hence i < s ; :: thesis: verum

end;

case s = i ; :: thesis: contradiction

then m + j <= m by A19, A27;
then j <= m - m by XREAL_1:21;
hence contradiction by A27; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

suppose ( r1 < s & s = r1 + 1 ) ; :: thesis: i < s

hence i < s by A31, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

suppose r1 = s ; :: thesis: i < s

hence i < s by A26, A28, A30; :: thesis: verum

end;

end;

end;

hence i < s ; :: thesis: verum

end;

end;

end;

A34: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A24, A25);
A35: ( 0 < k - m & m <= k ) by A19, XREAL_1:52;
reconsider l = k - m as Element of NAT by A19, INT_1:18;
m + l = k ;
hence i < r by A19, A34, A35; :: thesis: verum

end;

end;

end;

hence i < r ; :: thesis: verum