let i 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 > i holds

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

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 > i holds

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

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

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

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

assume that

A1: p in rng f and

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

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

A3: p .. f <= len f by A1, FINSEQ_4:21;

then A4: i <= len f by A2, XXREAL_0:2;

(p .. f) - i <= (len f) - i by A3, XREAL_1:9;

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

k <> 0 by A2;

then 1 <= k by NAT_1:14;

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

.= p by A1, FINSEQ_4:19 ;

then p .. (f /^ i) = k by A6, A7, Th2;

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

for p being Element of D

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

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

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 > i holds

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

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

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

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

assume that

A1: p in rng f and

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

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

A3: p .. f <= len f by A1, FINSEQ_4:21;

then A4: i <= len f by A2, XXREAL_0:2;

(p .. f) - i <= (len f) - i by A3, XREAL_1:9;

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

k <> 0 by A2;

then 1 <= k by NAT_1:14;

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

A7: now :: thesis: for j being Nat st 1 <= j & j < k holds

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

(f /^ i) . k =
f . (k + i)
by A4, A6, RFINSEQ:def 1
(f /^ i) . j <> (f /^ i) . k

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

assume that

A8: 1 <= j and

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

j <= i + j by NAT_1:11;

then A10: 1 <= i + j by A8, XXREAL_0:2;

i + k = p .. f ;

then A11: i + j < p .. f by A9, XREAL_1:6;

then i + j <= len f by A3, XXREAL_0:2;

then A12: i + j in dom f by A10, FINSEQ_3:25;

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

then j in dom (f /^ i) by A8, FINSEQ_3:25;

then A13: f . (i + j) = (f /^ i) . j by A4, RFINSEQ:def 1;

f . (i + k) = (f /^ i) . k by A4, A6, RFINSEQ:def 1;

hence (f /^ i) . j <> (f /^ i) . k by A1, A13, A11, A12, FINSEQ_4:19, FINSEQ_4:24; :: thesis: verum

end;assume that

A8: 1 <= j and

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

j <= i + j by NAT_1:11;

then A10: 1 <= i + j by A8, XXREAL_0:2;

i + k = p .. f ;

then A11: i + j < p .. f by A9, XREAL_1:6;

then i + j <= len f by A3, XXREAL_0:2;

then A12: i + j in dom f by A10, FINSEQ_3:25;

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

then j in dom (f /^ i) by A8, FINSEQ_3:25;

then A13: f . (i + j) = (f /^ i) . j by A4, RFINSEQ:def 1;

f . (i + k) = (f /^ i) . k by A4, A6, RFINSEQ:def 1;

hence (f /^ i) . j <> (f /^ i) . k by A1, A13, A11, A12, FINSEQ_4:19, FINSEQ_4:24; :: thesis: verum

.= p by A1, FINSEQ_4:19 ;

then p .. (f /^ i) = k by A6, A7, Th2;

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