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
(f /^ k) :- p = f :- p
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
(f /^ k) :- p = f :- p
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f > k holds
(f /^ k) :- p = f :- p
let f be FinSequence of D; :: thesis: ( p in rng f & p .. f > k implies (f /^ k) :- p = f :- p )
assume that
A1: p in rng f and
A2: p .. f > k ; :: thesis: (f /^ k) :- p = f :- p
thus (f /^ k) :- p = <*p*> ^ ((f /^ k) /^ (p .. (f /^ k))) by FINSEQ_5:def 2
.= <*p*> ^ (f /^ (k + (p .. (f /^ k)))) by Th81
.= <*p*> ^ (f /^ (p .. f)) by A1, A2, Lm3
.= f :- p by FINSEQ_5:def 2 ; :: thesis: verum