let D be non empty set ; :: thesis: for f being FinSequence of D
for p, q being Element of D st q in rng (f | (p .. f)) holds
q .. f <= p .. f
let f be FinSequence of D; :: thesis: for p, q being Element of D st q in rng (f | (p .. f)) holds
q .. f <= p .. f
let p, q be Element of D; :: thesis: ( q in rng (f | (p .. f)) implies q .. f <= p .. f )
assume A1: q in rng (f | (p .. f)) ; :: thesis: q .. f <= p .. f
then q .. (f | (p .. f)) = q .. f by FINSEQ_5:40;
then A2: q .. f <= len (f | (p .. f)) by A1, FINSEQ_4:21;
len (f | (p .. f)) <= p .. f by FINSEQ_5:17;
hence q .. f <= p .. f by A2, XXREAL_0:2; :: thesis: verum