let k be Nat; :: thesis: for D being non empty set

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies p .. f = k + (p .. (f /^ k)) )

assume that

A1: p in rng f and

A2: p .. f > k ; :: thesis: p .. f = k + (p .. (f /^ k))

reconsider i = (p .. f) - k as Element of NAT by A2, INT_1:5;

A3: i + k <= len f by A1, FINSEQ_4:21;

then A4: i <= (len f) - k by XREAL_1:19;

k <= k + i by NAT_1:11;

then k <= len f by A3, XXREAL_0:2;

then A5: i <= len (f /^ k) by A4, RFINSEQ:def 1;

i <> 0 by A2;

then 1 <= i by NAT_1:14;

then A6: i in dom (f /^ k) by A5, FINSEQ_3:25;

A7: k + i = p .. f ;

.= p by A1, FINSEQ_5:38 ;

then (p .. f) - k = p .. (f /^ k) by A6, A8, Th48;

hence p .. f = k + (p .. (f /^ k)) ; :: thesis: verum

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds

p .. f = k + (p .. (f /^ k))

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies p .. f = k + (p .. (f /^ k)) )

assume that

A1: p in rng f and

A2: p .. f > k ; :: thesis: p .. f = k + (p .. (f /^ k))

reconsider i = (p .. f) - k as Element of NAT by A2, INT_1:5;

A3: i + k <= len f by A1, FINSEQ_4:21;

then A4: i <= (len f) - k by XREAL_1:19;

k <= k + i by NAT_1:11;

then k <= len f by A3, XXREAL_0:2;

then A5: i <= len (f /^ k) by A4, RFINSEQ:def 1;

i <> 0 by A2;

then 1 <= i by NAT_1:14;

then A6: i in dom (f /^ k) by A5, FINSEQ_3:25;

A7: k + i = p .. f ;

A8: now :: thesis: for j being Nat st 1 <= j & j < i holds

(f /^ k) /. j <> (f /^ k) /. i

(f /^ k) /. i =
f /. (k + i)
by A6, FINSEQ_5:27
(f /^ k) /. j <> (f /^ k) /. i

let j be Nat; :: thesis: ( 1 <= j & j < i implies (f /^ k) /. j <> (f /^ k) /. i )

assume that

A9: 1 <= j and

A10: j < i ; :: thesis: (f /^ k) /. j <> (f /^ k) /. i

reconsider J = j as Nat ;

k + j >= j by NAT_1:11;

then A11: 1 <= k + j by A9, XXREAL_0:2;

j <= len (f /^ k) by A5, A10, XXREAL_0:2;

then j in dom (f /^ k) by A9, FINSEQ_3:25;

then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:27;

A13: k + i <= len f by A1, FINSEQ_4:21;

k + j < k + i by A10, XREAL_1:6;

then k + j <= len f by A13, XXREAL_0:2;

then A14: k + J in dom f by A11, FINSEQ_3:25;

k + j < p .. f by A7, A10, XREAL_1:6;

then A15: f /. (k + j) <> p by A14, FINSEQ_5:39;

f /. (k + i) = (f /^ k) /. i by A6, FINSEQ_5:27;

hence (f /^ k) /. j <> (f /^ k) /. i by A1, A12, A15, FINSEQ_5:38; :: thesis: verum

end;assume that

A9: 1 <= j and

A10: j < i ; :: thesis: (f /^ k) /. j <> (f /^ k) /. i

reconsider J = j as Nat ;

k + j >= j by NAT_1:11;

then A11: 1 <= k + j by A9, XXREAL_0:2;

j <= len (f /^ k) by A5, A10, XXREAL_0:2;

then j in dom (f /^ k) by A9, FINSEQ_3:25;

then A12: f /. (k + j) = (f /^ k) /. j by FINSEQ_5:27;

A13: k + i <= len f by A1, FINSEQ_4:21;

k + j < k + i by A10, XREAL_1:6;

then k + j <= len f by A13, XXREAL_0:2;

then A14: k + J in dom f by A11, FINSEQ_3:25;

k + j < p .. f by A7, A10, XREAL_1:6;

then A15: f /. (k + j) <> p by A14, FINSEQ_5:39;

f /. (k + i) = (f /^ k) /. i by A6, FINSEQ_5:27;

hence (f /^ k) /. j <> (f /^ k) /. i by A1, A12, A15, FINSEQ_5:38; :: thesis: verum

.= p by A1, FINSEQ_5:38 ;

then (p .. f) - k = p .. (f /^ k) by A6, A8, Th48;

hence p .. f = k + (p .. (f /^ k)) ; :: thesis: verum