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 number ; :: 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 b = b as Nat ;
A2: ( 1 <= b & b <= len g ) by A1, FINSEQ_3:25;
then 1 <= len g by XXREAL_0:2;
hence ( 1 in proj1 f & 1 c= b ) by A2, FINSEQ_3:25, NAT_1:39; :: thesis: verum