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

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