let i 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 & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & i in Seg (p .. f) holds
(f -: p) /. i = f /. i
let f be FinSequence of D; :: thesis: ( p in rng f & i in Seg (p .. f) implies (f -: p) /. i = f /. i )
assume that
A1: p in rng f and
A2: i in Seg (p .. f) ; :: thesis: (f -: p) /. i = f /. i
p .. f in dom f by A1, FINSEQ_4:20;
hence (f -: p) /. i = f /. i by A2, FINSEQ_4:71; :: thesis: verum