let k be Nat; 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 ; 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; 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; ( 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
; 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 for j being Nat st 1 <= j & j < i holds
(f /^ k) /. j <> (f /^ k) /. ilet j be
Nat;
( 1 <= j & j < i implies (f /^ k) /. j <> (f /^ k) /. i )assume that A9:
1
<= j
and A10:
j < i
;
(f /^ k) /. j <> (f /^ k) /. ireconsider 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;
verum end;
(f /^ k) /. i =
f /. (k + i)
by A6, FINSEQ_5:27
.=
p
by A1, FINSEQ_5:38
;
then
(p .. f) - k = p .. (f /^ k)
by A6, A8, Th48;
hence
p .. f = k + (p .. (f /^ k))
; verum