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 4;
f " {(f /. i)} c= dom f by RELAT_1:132;
then f " {(f /. i)} c= Seg (len f) by FINSEQ_1:def 3;
then a2: f " {(f /. i)} is included_in_Seg ;
assume A3: i in dom f ; :: thesis: (f /. i) .. f <= i
then f /. i = f . i by PARTFUN1:def 6;
then f . i in {(f /. i)} by TARSKI:def 1;
then i in f " {(f /. i)} by A3, FUNCT_1:def 7;
then i in rng (Sgm (f " {(f /. i)})) by a2, FINSEQ_1:def 14;
then consider l being object such that
A4: l in dom (Sgm (f " {(f /. i)})) and
A5: (Sgm (f " {(f /. i)})) . l = i by FUNCT_1:def 3;
reconsider l = l as Element of NAT by A4;
( 1 <= l & l <= len (Sgm (f " {(f /. i)})) ) by A4, FINSEQ_3:25;
hence (f /. i) .. f <= i by a2, A1, A5, FINSEQ_3:41; :: thesis: verum