let f be Function; :: thesis: ( f is T-Sequence-like implies f is segmental )
assume f is T-Sequence-like ; :: thesis: f is segmental
then reconsider f = f as T-Sequence ;
take dom f ; :: according to EXCHSORT:def 1 :: thesis: ex b being ordinal number st proj1 f = (dom f) \ b
take 0 ; :: thesis: proj1 f = (dom f) \ 0
thus proj1 f = (dom f) \ 0 ; :: thesis: verum