let f be Function; :: thesis: ( f is FinSequence-like implies f is 1 -based )
assume f is FinSequence-like ; :: thesis: f is 1 -based
then reconsider g = f as FinSequence ;
let b be Ordinal; :: according to EXCHSORT:def 2 :: thesis: ( b in proj1 f implies ( 1 in proj1 f & 1 c= b ) )
assume b in dom f ; :: thesis: ( 1 in proj1 f & 1 c= b )
then A1: b in dom g ;
then reconsider bb = b as Nat ;
A2: ( 1 <= bb & bb <= len g ) by A1, FINSEQ_3:25;
then A3: 1 <= len g by XXREAL_0:2;
thus 1 in proj1 f by FINSEQ_3:25, A3; :: thesis: 1 c= b
Segm 1 c= Segm bb by A2, NAT_1:39;
hence 1 c= b ; :: thesis: verum