let i 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 > i holds
i + (p .. (f /^ i)) = p .. f
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 > i holds
i + (p .. (f /^ i)) = p .. f
let p be 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 f be FinSequence of D; ( 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
; 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 for j being Nat st 1 <= j & j < k holds
(f /^ i) . j <> (f /^ i) . klet j be
Nat;
( 1 <= j & j < k implies (f /^ i) . j <> (f /^ i) . k )assume that A8:
1
<= j
and A9:
j < k
;
(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;
verum end;
(f /^ i) . k =
f . (k + i)
by A4, A6, RFINSEQ:def 1
.=
p
by A1, FINSEQ_4:19
;
then
p .. (f /^ i) = k
by A6, A7, Th2;
hence
i + (p .. (f /^ i)) = p .. f
; verum