let i be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i
let D be non empty set ; :: thesis: for f being FinSequence of D st i in dom f holds
(f /. i) .. f <= i
let f be FinSequence of D; :: thesis: ( i in dom f implies (f /. i) .. f <= i )
set p = f /. i;
A1: (f /. i) .. f = (Sgm (f " {(f /. i)})) . 1 by FINSEQ_4:def 5;
f " {(f /. i)} c= dom f by RELAT_1:167;
then A2: f " {(f /. i)} c= Seg (len f) by FINSEQ_1:def 3;
assume A3: i in dom f ; :: thesis: (f /. i) .. f <= i
then f /. i = f . i by PARTFUN1:def 8;
then f . i in {(f /. i)} by TARSKI:def 1;
then i in f " {(f /. i)} by A3, FUNCT_1:def 13;
then i in rng (Sgm (f " {(f /. i)})) by A2, FINSEQ_1:def 13;
then consider l being set such that
A4: l in dom (Sgm (f " {(f /. i)})) and
A5: (Sgm (f " {(f /. i)})) . l = i by FUNCT_1:def 5;
reconsider l = l as Element of NAT by A4;
( 1 <= l & l <= len (Sgm (f " {(f /. i)})) ) by A4, FINSEQ_3:27;
hence (f /. i) .. f <= i by A1, A2, A5, FINSEQ_3:46; :: thesis: verum