let f be Function; :: thesis: ( f is T-Sequence-like implies f is 0 -based )
assume f is T-Sequence-like ; :: thesis: f is 0 -based
then reconsider g = f as T-Sequence ;
let b be ordinal number ; :: according to EXCHSORT:def 2 :: thesis: ( b in proj1 f implies ( 0 in proj1 f & 0 c= b ) )
assume b in dom f ; :: thesis: ( 0 in proj1 f & 0 c= b )
then b in dom g ;
hence ( 0 in proj1 f & 0 c= b ) by ORDINAL3:8; :: thesis: verum