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) holds
p .. (f | i) = p .. f
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) holds
p .. (f | i) = p .. f
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng (f | i) holds
p .. (f | i) = p .. f
let f be FinSequence of D; :: thesis: ( p in rng (f | i) implies p .. (f | i) = p .. f )
A1: dom (f | i) c= dom f by Th18;
assume A2: p in rng (f | i) ; :: thesis: p .. (f | i) = p .. f
then A3: p .. (f | i) in dom (f | i) by FINSEQ_4:20;
then f /. (p .. (f | i)) = (f | i) /. (p .. (f | i)) by FINSEQ_4:70
.= p by A2, Th38 ;
then A4: p .. f <= p .. (f | i) by A3, A1, Th39;
p .. (f | i) <= len (f | i) by A2, FINSEQ_4:21;
then A5: p .. f <= len (f | i) by A4, XXREAL_0:2;
A6: rng (f | i) c= rng f by Th19;
then 1 <= p .. f by A2, FINSEQ_4:21;
then A7: p .. f in dom (f | i) by A5, FINSEQ_3:25;
then (f | i) /. (p .. f) = f /. (p .. f) by FINSEQ_4:70
.= p by A2, A6, Th38 ;
then p .. (f | i) <= p .. f by A7, Th39;
hence p .. (f | i) = p .. f by A4, XXREAL_0:1; :: thesis: verum