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
(f /^ k) -: p = (f -: p) /^ 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
(f /^ k) -: p = (f -: p) /^ k
let p be Element of D; for f being FinSequence of D st p in rng f & p .. f > k holds
(f /^ k) -: p = (f -: p) /^ k
let f be FinSequence of D; ( p in rng f & p .. f > k implies (f /^ k) -: p = (f -: p) /^ k )
assume that
A1:
p in rng f
and
A2:
p .. f > k
; (f /^ k) -: p = (f -: p) /^ k
A3:
p in rng (f /^ k)
by A1, A2, Th62;
p .. f = k + (p .. (f /^ k))
by A1, A2, Th61;
then A4: len ((f /^ k) -: p) =
(p .. f) - k
by A3, FINSEQ_5:45
.=
(len (f -: p)) - k
by A1, FINSEQ_5:45
;
A5:
now let m be
Nat;
( m in dom ((f /^ k) -: p) implies ((f /^ k) -: p) . m = (f -: p) . (m + k) )A6:
m + k >= m
by NAT_1:11;
reconsider M =
m as
Element of
NAT by ORDINAL1:def 13;
assume A7:
m in dom ((f /^ k) -: p)
;
((f /^ k) -: p) . m = (f -: p) . (m + k)then
m <= (len (f -: p)) - k
by A4, FINSEQ_3:27;
then A8:
m + k <= len (f -: p)
by XREAL_1:21;
1
<= m
by A7, FINSEQ_3:27;
then
1
<= m + k
by A6, XXREAL_0:2;
then A9:
M + k in dom (f -: p)
by A8, FINSEQ_3:27;
len ((f /^ k) -: p) = p .. (f /^ k)
by A3, FINSEQ_5:45;
then A10:
m in Seg (p .. (f /^ k))
by A7, FINSEQ_1:def 3;
(f /^ k) -: p = (f /^ k) | (p .. (f /^ k))
by FINSEQ_5:def 1;
then A11:
dom ((f /^ k) -: p) c= dom (f /^ k)
by FINSEQ_5:20;
len (f -: p) = p .. f
by A1, FINSEQ_5:45;
then A12:
m + k in Seg (p .. f)
by A9, FINSEQ_1:def 3;
thus ((f /^ k) -: p) . m =
((f /^ k) -: p) /. m
by A7, PARTFUN1:def 8
.=
(f /^ k) /. m
by A3, A10, FINSEQ_5:46
.=
f /. (m + k)
by A7, A11, FINSEQ_5:30
.=
(f -: p) /. (M + k)
by A1, A12, FINSEQ_5:46
.=
(f -: p) . (m + k)
by A9, PARTFUN1:def 8
;
verum end;
k <= len (f -: p)
by A1, A2, FINSEQ_5:45;
hence
(f /^ k) -: p = (f -: p) /^ k
by A4, A5, RFINSEQ:def 2; verum