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 )
assume A1: p in rng (f | i) ; :: thesis: p .. (f | i) = p .. f
then A2: p .. (f | i) in dom (f | i) by FINSEQ_4:30;
A3: dom (f | i) c= dom f by Th20;
A4: rng (f | i) c= rng f by Th21;
f /. (p .. (f | i)) = (f | i) /. (p .. (f | i)) by A2, FINSEQ_4:85
.= p by A1, Th41 ;
then A5: p .. f <= p .. (f | i) by A2, A3, Th42;
A6: 1 <= p .. f by A1, A4, FINSEQ_4:31;
p .. (f | i) <= len (f | i) by A1, FINSEQ_4:31;
then p .. f <= len (f | i) by A5, XXREAL_0:2;
then A7: p .. f in dom (f | i) by A6, FINSEQ_3:27;
then (f | i) /. (p .. f) = f /. (p .. f) by FINSEQ_4:85
.= p by A1, A4, Th41 ;
then p .. (f | i) <= p .. f by A7, Th42;
hence p .. (f | i) = p .. f by A5, XXREAL_0:1; :: thesis: verum