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 ) )
defpred S1[ Element of NAT ] means ( $1 in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = $1 ) );
A6: 0 + 1 <= len v by A1, NAT_1:13;
then A7: len v in dom v by FINSEQ_3:25;
A8: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A9: ( i in Seg n implies ex k being Element of NAT st
( k in dom v & v . k = i ) ) ; :: thesis: S1[i + 1]
assume A10: 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 A11: 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, A11, FINSEQ_3:25; :: thesis: verum
end;
suppose A12: i <> 0 ; :: thesis: ex k being Element of NAT st
( k in dom v & v . k = i + 1 )
defpred S2[ set ] means ( $1 in dom v & v . $1 = i );
A13: for k being Nat st S2[k] holds
k <= len v by FINSEQ_3:25;
i + 1 <= n by A10, FINSEQ_1:1;
then A14: i <= n by NAT_1:13;
A15: 0 + 1 <= i by A12, NAT_1:13;
then A16: ex k being Nat st S2[k] by A9, A14, FINSEQ_1:1;
consider m being Nat such that
A17: ( S2[m] & ( for k being Nat st S2[k] holds
k <= m ) ) from NAT_1:sch 6(A13, A16);
A18: for k being Element of NAT st S2[k] holds
k <= m by A17;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take k = m + 1; :: thesis: ( k in dom v & v . k = i + 1 )
i in Seg n by A15, A14, FINSEQ_1:1;
hence ( k in dom v & v . k = i + 1 ) by A1, A2, A4, A5, A10, A17, A18, Th85; :: thesis: verum
end;
end;
end;
hence ex k being Element of NAT st
( k in dom v & v . k = i + 1 ) ; :: thesis: verum
end;
A19: S1[ 0 ] by FINSEQ_1:1;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A19, A8); :: 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 that
A20: m in dom v and
A21: v . m = i and
A22: for j being Element of NAT st j in dom v & v . j = i holds
j <= m and
A23: m < k and
A24: k in dom v and
A25: r = v . k ; :: thesis: i < r
A26: ( m <= len v & k <= len v ) by A20, A24, FINSEQ_3:25;
A27: 1 <= m by A20, FINSEQ_3:25;
A28: i in rng v by A20, A21, FUNCT_1:def 3;
then A29: i <= n by A2, FINSEQ_1:1;
now
per cases ( i = n or i <> n ) ;
suppose i = n ; :: thesis: i < r
then len v <= m by A4, A7, A22;
hence i < r by A23, A26, XXREAL_0:1; :: thesis: verum
end;
suppose A30: i <> n ; :: thesis: i < r
defpred S2[ 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;
i < n by A29, A30, 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:1;
then A31: v . (m + 1) = i + 1 by A1, A2, A4, A5, A20, A21, A22, A28, Th85;
A32: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A33: S2[k] ; :: thesis: S2[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 that
A34: j = k + 1 and
A35: j > 0 and
A36: m + j in dom v and
A37: s = v . (m + j) ; :: thesis: i < s
per cases ( k = 0 or k <> 0 ) ;
suppose A38: k <> 0 ; :: thesis: i < s
m <= m + k by NAT_1:11;
then A39: 1 <= m + k by A27, XXREAL_0:2;
s in rng v by A36, A37, FUNCT_1:def 3;
then s in Seg n by A2;
then reconsider s1 = s as Element of NAT ;
A40: m + (k + 1) <= len v by A34, A36, FINSEQ_3:25;
m + k <= (m + k) + 1 by NAT_1:11;
then m + k <= len v by A40, XXREAL_0:2;
then A41: m + k in dom v by A39, FINSEQ_3:25;
then v . (m + k) in rng v by FUNCT_1:def 3;
then v . (m + k) in Seg n by A2;
then reconsider r1 = v . (m + k) as Element of NAT ;
A42: i < r1 by A33, A38, A41;
A43: (m + k) + 1 = m + (k + 1) ;
then A44: m + k <= (len v) - 1 by A40, XREAL_1:19;
now
per cases ( abs (r1 - s) = 1 or r1 = s ) by A5, A34, A37, A43, A39, A44;
suppose A45: abs (r1 - s) = 1 ; :: thesis: i < s
now
per cases ( ( r1 > s & r1 = s + 1 ) or ( r1 < s & s = r1 + 1 ) ) by A45, Th81;
suppose ( r1 > s & r1 = s + 1 ) ; :: thesis: i < s
then A46: i <= s1 by A42, NAT_1:13;
now
per cases ( i < s or s = i ) by A46, XXREAL_0:1;
case i < s ; :: thesis: i < s
hence i < s ; :: thesis: verum
end;
end;
end;
hence i < s ; :: thesis: verum
end;
suppose ( r1 < s & s = r1 + 1 ) ; :: thesis: i < s
hence i < s by A42, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence i < s ; :: thesis: verum
end;
suppose r1 = s ; :: thesis: i < s
hence i < s by A33, A38, A41; :: thesis: verum
end;
end;
end;
hence i < s ; :: thesis: verum
end;
end;
end;
reconsider l = k - m as Element of NAT by A23, INT_1:5;
A47: ( 0 < k - m & m + l = k ) by A23, XREAL_1:50;
A48: S2[ 0 ] ;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A48, A32);
hence i < r by A24, A25, A47; :: thesis: verum
end;
end;
end;
hence i < r ; :: thesis: verum